Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update to Isabelle2024 #764

Merged
merged 6 commits into from
Jun 12, 2024
Merged

Update to Isabelle2024 #764

merged 6 commits into from
Jun 12, 2024

Commits on Jun 12, 2024

  1. word_lib: import changes from afp-2024 

    Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37 @corlewis
    lsf37 authored and corlewis committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    fef1694 View commit details
    Browse the repository at this point in the history

  2. lib+asmrefine+autocorres+c-parser+proof: update to Isabelle2024 

    - Exn.interruptible_capture has been renamed to Exn.result.
- simproc setup has changed slightly
- can no longer catch all exceptions
- Term_Subst renames
- Global_Theory.add_defs was downgraded to Global_Theory.add_def

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
    @corlewis @lsf37
    corlewis and lsf37 committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    45a1c4c View commit details
    Browse the repository at this point in the history

  3. lib: update old-style "defs" to Isabelle2024 

    The old Global_Theory.add_defs command lost some options and no longer
processes attributes. This commit reflects these changes up into the
"defs" command:

- remove "overloading" and "unchecked" options
- remove attribute spec -- use pure binding for thm name
- only one equation per "defs" command
- remove deprecation warning, because we are using this command
  intentionally
- document these changes in the header

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37 @corlewis
    lsf37 authored and corlewis committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    dbfcc43 View commit details
    Browse the repository at this point in the history

  4. design/skel: update for changed defs command 

    Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
    @corlewis
    corlewis committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    5314636 View commit details
    Browse the repository at this point in the history

  5. c-parser: more tweaks to table.ML for Isabelle2024 

    src/Pure/General/table.ML in Isabelle2024 has a new function
unsynchronized_cache which draws in further Isabelle library features
that we have so far not included in the standalone parser. The new
function isn't used in the standalone parser, so we remove it from
the signature and struct in the copying process.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37 @corlewis
    lsf37 authored and corlewis committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    37fd1f7 View commit details
    Browse the repository at this point in the history

  6. c-parser: make table.ML depend on Makefile 

    Since the contents of the generated table.ML depend on the Makefile,
the Makefile itself should be a dependency.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
    @lsf37 @corlewis
    lsf37 authored and corlewis committed Jun 12, 2024
    Configuration menu
    Copy the full SHA
    1b9009d View commit details
    Browse the repository at this point in the history