Add ACL2-Jupyter devcontainer and Jupyter notebook conversion and book certification helper. #1
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Add .devcontainer for ghcr.io/jimwhite/acl2-jupyter:latest (source https://github.com/jimwhite/acl2-jupyter) which is a multiplatform Docker image for running ACL2 in Ubuntu using SBCL and includes Z3 (for SMTLink) and NodeJS (for easy Claude Code install). The project dir includes how to for running on GitHub Codespaces (for free!).
Convert all .lisp ACL2 books to .ipynb ACL2 notebooks and run them all to display outputs.
Added a certify books helper to the Makefile so including books works.
TODO: Add direction flag so that .ipynb files can be the sources instead of the targets for conversion. In the meantime Jupyter's "File > Save & Export ... > As Executable Script" works.
Thank you very much Mike! This is a great start on automating ACL2 and I struggled (and failed) to get CC to make a working ACL2 MCP and look forward to giving yours a whirl.