diff options
| author | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-25 17:58:26 +0000 |
|---|---|---|
| committer | Thomas Bauereiss <tb592@cl.cam.ac.uk> | 2019-11-25 17:58:26 +0000 |
| commit | 09acf70118de41e04dab37977daae56c6349dfec (patch) | |
| tree | 8a6236f39fef06314676693d845176b279595943 /Makefile | |
| parent | 1a653fc6207b8cb20204af6b2ccabab48a020945 (diff) | |
| download | sail-riscv-09acf70118de41e04dab37977daae56c6349dfec.zip sail-riscv-09acf70118de41e04dab37977daae56c6349dfec.tar.gz sail-riscv-09acf70118de41e04dab37977daae56c6349dfec.tar.bz2 | |
Work around Isabelle problem in PTW functions
The standard pattern completeness proof for recursive functions
generated by Lem for Isabelle seems to get confused in some situations
when there are variables with unit type (in particular the ext_ptw
argument of the page table walk functions). Solving this properly
requires some more digging into the Isabelle simplifier, but the ad-hoc
workaround in this commit fixes the problem for now.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -255,6 +255,7 @@ generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle generated_definitions/lem/$(ARCH)/riscv.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/$(ARCH)/Riscv_types.thy sed -i "s/record( 'asidlen, 'valen, 'palen, 'ptelen) TLB_Entry/record (overloaded) ( 'asidlen, 'valen, 'palen, 'ptelen) TLB_Entry/" generated_definitions/isabelle/$(ARCH)/Riscv_types.thy + sed -i "s/by pat_completeness auto/by pat_completeness (auto intro!: let_cong bind_cong MemoryOpResult.case_cong)/" generated_definitions/isabelle/$(ARCH)/Riscv.thy generated_definitions/hol4/$(ARCH)/Holmakefile: handwritten_support/Holmakefile mkdir -p generated_definitions/hol4/$(ARCH) |