Merge pull request 'chore: Version bump and toolchain cleanup' (#51) from misc/toolchain into dev
Reviewed-on: #51
This commit is contained in:
commit
aeed233846
16
README.md
16
README.md
|
@ -1,9 +1,12 @@
|
|||
# Pantograph
|
||||
|
||||
An interaction system for Lean 4.
|
||||
A Machine-to-Machine interaction system for Lean 4.
|
||||
|
||||
![Pantograph](doc/icon.svg)
|
||||
|
||||
Pantograph provides interfaces to execute proofs, construct expressions, and
|
||||
examine the symbol list of a Lean project for machine learning.
|
||||
|
||||
## Installation
|
||||
|
||||
For Nix based workflow, see below.
|
||||
|
@ -109,9 +112,12 @@ ulimit -s unlimited
|
|||
## Library Usage
|
||||
|
||||
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
|
||||
with `Pantograph`.
|
||||
with `Pantograph` which mirrors the REPL commands above. It is recommended to
|
||||
call Pantograph via this FFI since it provides a tremendous speed up.
|
||||
|
||||
## Testing
|
||||
## Developing
|
||||
|
||||
### Testing
|
||||
|
||||
The tests are based on `LSpec`. To run tests,
|
||||
``` sh
|
||||
|
@ -120,6 +126,10 @@ make test
|
|||
|
||||
## Nix based workflow
|
||||
|
||||
The included Nix flake provides build targets for `sharedLib` and `executable`.
|
||||
The executable can be used as-is, but linking against the shared library
|
||||
requires the presence of `lean-all`.
|
||||
|
||||
To run tests:
|
||||
``` sh
|
||||
nix build .#checks.${system}.test
|
||||
|
|
14
flake.nix
14
flake.nix
|
@ -37,9 +37,14 @@
|
|||
};
|
||||
project = leanPkgs.buildLeanPackage {
|
||||
name = "Pantograph";
|
||||
#roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ];
|
||||
roots = [ "Main" "Pantograph" ];
|
||||
src = ./.;
|
||||
src = pkgs.lib.cleanSourceWith {
|
||||
src = ./.;
|
||||
filter = path: type:
|
||||
!(pkgs.lib.hasInfix "/Test/" path) &&
|
||||
!(pkgs.lib.hasSuffix ".md" path) &&
|
||||
!(pkgs.lib.hasSuffix "Makefile" path);
|
||||
};
|
||||
};
|
||||
test = leanPkgs.buildLeanPackage {
|
||||
name = "Test";
|
||||
|
@ -58,7 +63,6 @@
|
|||
packages = {
|
||||
inherit (leanPkgs) lean lean-all;
|
||||
inherit (project) sharedLib executable;
|
||||
test = test.executable;
|
||||
default = project.executable;
|
||||
};
|
||||
checks = {
|
||||
|
@ -69,7 +73,9 @@
|
|||
${test.executable}/bin/test > $out
|
||||
'';
|
||||
};
|
||||
devShells.default = project.devShell;
|
||||
devShells.default = pkgs.mkShell {
|
||||
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
|
||||
};
|
||||
};
|
||||
};
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue