Nikolaus Huber (Sep 21 2026 at 21:54): Nikolaus Huber (Sep 21 2026 at 21:54):I already posted this on the Isabelle mailing list, but thought I would copy it here as well:
We have been working on a Python backend for the Isabelle code generator, and I believe it has reached a level of maturity that it might be useful to other people as well:
https://github.com/pure-py/isabelle-python-codegen
We are roughly targeting a pure, functional subset of Python we termed PurePy (https://pure-py.github.io), which is a proper subset of Python 3.12+.
Two different Python code extraction setups are provided: Python.Python uses only a minimal set of custom code printing, while Python.Python_Setup includes custom code printers to utilise native Python ints, lists, and tuples.
As this is my first time working with Isabelle in this manner, I am grateful for any feedback. I have ported the test suite from the Go backend, so a sizeable section of the HOL library is tested. Eventually, after some more testing, we would like to create a submission to the AFP as well.
Last updated: Oct 05 2026 at 16:54 UTC