Awesome
Proof Pad
Proof Pad is a web based IDE for ACL2, using Google Kubernetes Engine to run ACL2 itself on the backend. Users can write and verify functions and theorems using a modern editor or a REPL interface. It's the evolution of the original Proof Pad project.
This is not an official Google product.
Deploying the frontend
- Run
rm -r dist grammar && ./grammar.sh && npx parcel build index.html
- Copy the contents of dist to Google Cloud Storage
Deploying the backend
- Update the ACL2 version in the Dockerfile if necessary.
- Run:
This takes about 30 minutes. If your terminal disconnects, check https://console.cloud.google.com/cloud-build/builds?project=proof-pad for the status$ gcloud builds submit --project=proof-pad --tag=us-central1-docker.pkg.dev/proof-pad/acl2/acl2 --timeout=86400s --machine-type=N1_HIGHCPU_8 .
- Go to this page and deploy a new revision with the build.