Something went wrong. Try again.
lol
Something went wrong. Try again.
1.8 kB · 67 lines
Nix
at master
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768{ lib, buildLakePackage, fetchFromGitHub, fetchNpmDeps, npmHooks, nodejs,}:
let version = "0.0.95"; src = fetchFromGitHub { owner = "leanprover-community"; repo = "ProofWidgets4"; tag = "v${version}"; hash = "sha256-LETljr+QEU6CxprR3pB4hUzhgCD8PrIuiPOgTIdhHVM="; };in
buildLakePackage { pname = "lean4-proofwidgets"; inherit version src;
leanPackageName = "proofwidgets";
# ProofWidgets has no Lean dependencies (lake-manifest.json packages = []). lakeHash = null;
nativeBuildInputs = [ nodejs npmHooks.npmConfigHook ];
# Pre-fetched npm dependencies for the TypeScript widget build # (npm/rollup in widget/). npmConfigHook installs these offline. npmDeps = fetchNpmDeps { name = "lean4-proofwidgets-npm-deps"; inherit src; sourceRoot = "source/widget"; hash = "sha256-ShH6MDr76wzWQrJvhMWCnklaox/uRsfoe+aYVSo/eNA="; }; npmRoot = "widget";
# Lake's widgetJsAll target runs `npm clean-install` which wipes # node_modules and the patched shebangs that npmConfigHook applied. # Wrap npm to skip ci/clean-install (deps already installed) while # passing `npm run build` through — same pattern as llama-cpp/evcc. postConfigure = '' local realNpm realNpm="$(type -P npm)" mkdir -p "$TMPDIR/npm-wrap" cat > "$TMPDIR/npm-wrap/npm" <<WRAPPER #!/bin/sh case "\$1" in ci|clean-install) exit 0 ;; esac exec "$realNpm" "\$@" WRAPPER chmod +x "$TMPDIR/npm-wrap/npm" export PATH="$TMPDIR/npm-wrap:$PATH" '';
meta = { description = "Interactive UI framework for Lean 4 proof assistants"; homepage = "https://github.com/leanprover-community/ProofWidgets4"; license = lib.licenses.asl20; maintainers = with lib.maintainers; [ nadja-y ]; };}