This project aims to build a few Python-based compilers for simple languages (Ari, Arisu, ArisuS), with formal verifications done using Dafny. The verified code will be generated as Python code (to be intergrated with the rest of the compilers).
The initial language (which we call Ari) is based on one of the examples officially provided by Dafny.
We used VSCode as the main IDE for the development of the compiler. The Python profile template was used to set up the environment; then ANTLR4 grammar syntax support and Dafny extensions were installed.
AI-assisted coding was enabled using Github Copilot, and external use of AI tools like ChatGPT was also used in the development.
- Note: You can do testing and drafting code by creating a
testzonefolder in the root directory, as.gitignoreis set to ignore this folder.
For non-technical work:
- Markdown extension pack and Github Markdown Preview for writing the documentation.
- Note: Instant Markdown is removed since weird "pop out browser" behavior keeps happening.
- Note:
ocamllanguage annotation todafnycode blocks to enable syntax highlighting.
- nyan-mode for the cute and funny nyan cat progress bar.
- Doki Theme for the cute and funny anime themes and backgrounds.
To reproduce the given environment, you can install the extensions yourself, or create a new VSCode profile based on the file .vscode/DafnyDevEnv (With ANTLR 4 and Python 3).code-profile in this repository.
-
The Python 3.11 environment is managed using uv, with dependencies such as
antlr4-python3-runtime>=4.13.2anddafnyruntimepython>=4.9.0. More information can be found in thepyproject.tomlfile. -
The generated Dafny code is expected to be Python 3.7 compatible (as of Dafny 4.9.0), while the Python environment is set to 3.11. Further compatibility checks will be done in the future, as for now, the generated code is still integrated with the Python codebase.