A Fork of AutoCorres

This repository is a fork of the seL4/l4v repository. The main purpose is to maintain a local version of AutoCorres.

Each feature changed with respect to the upstream repository is tracked on its own branch.

The main brach (called "master") contains all features from the individual feature branches described below:

Active Branches

Branch "autogenerated_parser"

This branch adds the C-parser files generated by mllex and mlyacc to reduce dependencies required by users of AutoCorres.

Branch "renaming_Word_Lib"

This branch renames the session Word_Lib shipped by AutoCorres to Word_Lib_l4v to avoid a name clash with the AFP entry of same name. This allows one to use AutoCorres with the AFP being registered as an Isabelle component.

Branch "cpp_wrapper"

This branch adds an OS check to the cpp-wrapper script. This allows using the cpp wrapper on all supported operating systems, allowing a uniform declare [[cpp_path = "..."]] across all supported operating systems.

Obsolete Branches

Branch "cpp_path_relative"

This branch converts a relative cpp_path (e.g., declare [[cpp_path = "tools/cpp_wrapper"]] into an absolute path, relative to the theory using install_C_file. This minimized the need for local configuration that cannot be easily shared within a development team. This branch is now obsolete, as the corresponding PR has been accepted upstream.

Branch "umm_types_realtive"

Ensure that umm_types.txt is saved relative to theory file. This branch is now obsolete, as the corresponding PR has been accepted upstream.

Branch "isabelle2023"

This branch provides a port of AutoCorres (and AutoCorres only) to Isabelle 2023. This branch is now obsolete, as the upstream repository supports Isabelle 2023.