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

making progres, put header in output of toy model, then about to execute lean so need to figure out how pypanto wants src hdear and thm

This commit is contained in:
Brando Miranda 2024-06-03 12:50:41 -07:00
parent c73e56630e
commit 18ebf0bb7d
2 changed files with 13 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
README.md
View File

@ -3,49 +3,20 @@
Python interface to the Pantograph library
# Getting started
<!-- Update submodule
``` bash
git submodule update --init
```
Install dependencies
```bash
poetry install
``` -->
<!-- First initialize the git submodules so that git can keep track of the submodules being used do:
```bash
# - initialize the git submodules by preparing the git repository, but it does not clone or fetch them, just init's git's internal configs
git submodule init
```
Then to clone, fetch & update the submodules code (and also initilize anything you might have forgotten that is specificed in the `.gitmodules` file):
```bash
# - initialize the git submodules so that git can track them and then the update clone/fetches & updates the submodules
git submodule update --init
```
Then install poetry by (e.g., [by following poetry's official instructions](https://python-poetry.org/docs/#installing-manually)).
Then once you confirm you have poetry & the initialized git submodules, execute:
```bash
poetry build
```
To run server tests:
``` bash
python -m pantograph.server
```
The tests in `pantograph/server.py` also serve as simple interaction examples -->
## Install 1: With Conda and Pip in the SNAP cluster
```bash
# - Install Lean4 manually (elan and lake), 1st one is the SNAP one, 2nd is the most common one
# - Install Lean 4 manually (elan & lake): gets install script (doesn't save it) & directly gives it to sh to install it
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y
# (install command from the Lean4 official instlal guide, not the one we use)
# curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s
# - Make sure Lean4 tools (lean, lake) are available
echo $PATH | tr ':' '\n'
export PATH="$HOME/.elan/bin:$PATH"
echo 'export PATH="$HOME/.elan/bin:$PATH"' >> ~/.bashrc
bash
# bash
elan
lake

12
build.py
View File

@ -3,13 +3,19 @@
import subprocess, shutil, os, stat
from pathlib import Path
# -- Install Panograph
# Define paths for Pantograph source and Pantograph Python interface
PATH_PANTOGRAPH = Path("./src")
PATH_PY = Path("./pantograph")
# Run the `make` command in the PATH_PANTOGRAPH directory to build the Pantograph executable
with subprocess.Popen(["make"], cwd=PATH_PANTOGRAPH) as p:
p.wait()
# Define the path to the executable
path_executable = PATH_PY / "pantograph"
# Copy the built Pantograph executable to the specified path
shutil.copyfile(PATH_PANTOGRAPH / ".lake/build/bin/pantograph", path_executable)
# Change the permissions of the Pantograph executable to make it executable
os.chmod(path_executable, os.stat(path_executable).st_mode | stat.S_IEXEC)
shutil.copyfile(PATH_PANTOGRAPH / "lean-toolchain", PATH_PY / "lean-toolchain")
# -- Copy the Lean toolchain file to the specified path
shutil.copyfile(PATH_PANTOGRAPH / "lean-toolchain", PATH_PY / "lean-toolchain")