aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 2 Pull Requests Packages Projects Releases 1 Wiki Activity

Merge pull request 'chore: Version bump and toolchain cleanup' (#51) from misc/toolchain into dev 

Reviewed-on: #51
This commit is contained in:
Leni Aniva 2024-03-28 22:36:25 -07:00
parent 431e81ca2f 2ea8b1c73c
commit 14011945a0
2 changed files with 23 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
README.md
View File

@ -1,9 +1,12 @@
# Pantograph # Pantograph
An interaction system for Lean 4. A Machine-to-Machine interaction system for Lean 4.
![Pantograph](doc/icon.svg) ![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 ## Installation
For Nix based workflow, see below. For Nix based workflow, see below.
@ -109,9 +112,12 @@ ulimit -s unlimited
## Library Usage ## Library Usage
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call `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, The tests are based on `LSpec`. To run tests,
``` sh ``` sh
@ -120,6 +126,10 @@ make test
## Nix based workflow ## 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: To run tests:
``` sh ``` sh
nix build .#checks.${system}.test nix build .#checks.${system}.test

14
flake.nix
View File

@ -37,9 +37,14 @@
}; };
project = leanPkgs.buildLeanPackage { project = leanPkgs.buildLeanPackage {
name = "Pantograph"; name = "Pantograph";
#roots = pkgs.lib.optional pkgs.stdenv.isDarwin [ "Main" "Pantograph" ];
roots = [ "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 { test = leanPkgs.buildLeanPackage {
name = "Test"; name = "Test";
@ -58,7 +63,6 @@
packages = { packages = {
inherit (leanPkgs) lean lean-all; inherit (leanPkgs) lean lean-all;
inherit (project) sharedLib executable; inherit (project) sharedLib executable;
test = test.executable;
default = project.executable; default = project.executable;
}; };
checks = { checks = {
@ -69,7 +73,9 @@
${test.executable}/bin/test > $out ${test.executable}/bin/test > $out
''; '';
}; };
devShells.default = project.devShell; devShells.default = pkgs.mkShell {
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
};
}; };
}; };
} }