Nadja Yang
b606786817
Add leangz (leantar) as a new build and runtime dependency. https://github.com/leanprover/lean4/releases/tag/v4.30.0 https://github.com/leanprover-community/mathlib4/blob/v4.30.0/lake-manifest.json
59 lines
1.3 KiB
Nix
59 lines
1.3 KiB
Nix
{
|
|
lib,
|
|
buildLakePackage,
|
|
fetchFromGitHub,
|
|
fetchNpmDeps,
|
|
npmHooks,
|
|
nodejs,
|
|
}:
|
|
|
|
buildLakePackage (finalAttrs: {
|
|
pname = "lean4-proofwidgets";
|
|
# nixpkgs-update: no auto update
|
|
version = "0.0.99";
|
|
|
|
src = fetchFromGitHub {
|
|
owner = "leanprover-community";
|
|
repo = "ProofWidgets4";
|
|
tag = "v${finalAttrs.version}";
|
|
hash = "sha256-kGoEkKGrucNUWFYkHW2LsS1gI4C0J8bAHQL2MiE4Pzc=";
|
|
};
|
|
|
|
leanPackageName = "proofwidgets";
|
|
|
|
lakeHash = null;
|
|
|
|
nativeBuildInputs = [
|
|
nodejs
|
|
npmHooks.npmConfigHook
|
|
];
|
|
|
|
npmDeps = fetchNpmDeps {
|
|
name = "lean4-proofwidgets-npm-deps";
|
|
src = finalAttrs.src;
|
|
sourceRoot = "source/widget";
|
|
hash = "sha256-ssWSr2qfsIbX25DidiVPm0tsLGjrhQhQ6YKPL0rfc1k=";
|
|
};
|
|
npmRoot = "widget";
|
|
|
|
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 ];
|
|
};
|
|
})
|