secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

lib: make ML_Utils a separate session 

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-01-20 11:56:32 +11:00
parent f0f19375f7
commit d86d577657
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
15 changed files with 58 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
ROOTS
View File

@ -7,6 +7,7 @@ tools
camkes
sys-init
lib
lib/ML_Utils
lib/Word_Lib
lib/sep_algebra
lib/EVTutorial

3
lib/Apply_Trace.thy
View File

@ -8,8 +8,7 @@
* Provides an alternate refinement function which takes an additional stateful journaling operation. *)
theory Apply_Trace
imports
Main
"MLUtils"
ML_Utils.MLUtils
begin

2
lib/Crunch.thy
View File

@ -8,7 +8,7 @@ theory Crunch
imports
WPSimp
Lib
MLUtils
ML_Utils.MLUtils
keywords "crunch" "crunch_ignore" "crunches" :: thy_decl
begin

4
lib/FP_Eval.thy
View File

@ -6,8 +6,8 @@
theory FP_Eval
imports
HOL.HOL
TermPatternAntiquote
HOL.HOL (* FIXME lib: remove *)
ML_Utils.TermPatternAntiquote
begin
text \<open>

2
lib/ML_Goal_Test.thy
View File

@ -7,7 +7,7 @@
theory ML_Goal_Test
imports
ML_Goal
MLUtils
ML_Utils.MLUtils
begin
experiment begin

4
lib/ML_Utils/MkTermAntiquote_Tests.thy
View File

@ -9,8 +9,8 @@ text \<open>
\<close>
theory MkTermAntiquote_Tests
imports
Lib.MkTermAntiquote
Main
MkTermAntiquote
Main (* MkTermAntiquote imports only Pure *)
begin
text \<open>

18
lib/ML_Utils/ROOT Normal file
View File

@ -0,0 +1,18 @@
(*
* Copyright 2023, Proofcraft Pty Ltd
*
* SPDX-License-Identifier: BSD-2-Clause
*)
chapter Lib
session ML_Utils (lib) = HOL +
theories
MLUtils
MkTermAntiquote
TermPatternAntiquote
TacticAntiquotation
TacticTutorial
MkTermAntiquote_Tests
TacticAntiquotation_Test
TermPatternAntiquote_Tests

2
lib/ML_Utils/TacticAntiquotation_Test.thy
View File

@ -8,7 +8,7 @@
theory TacticAntiquotation_Test
imports
Lib.TacticAntiquotation
TacticAntiquotation
begin
text \<open>Simple tests.\<close>

4
lib/ML_Utils/TermPatternAntiquote_Tests.thy
View File

@ -6,8 +6,8 @@
theory TermPatternAntiquote_Tests
imports
Lib.TermPatternAntiquote
Main
TermPatternAntiquote
Main (* TermPatternAntiquote imports only Pure *)
begin
text \<open>

22
lib/ML_Utils/tests.xml Normal file
View File

@ -0,0 +1,22 @@
<?xml version="1.0"?>
<!--
Copyright 2023, Proofcraft Pty Ltd
SPDX-License-Identifier: BSD-2-Clause
-->
<!--
Regression Specification File
See "misc/regression/tests.xml" for a description of the file
format.
-->
<testsuite cpu-timeout="600">
<set depends="isabelle">
<test name="ML_Utils">../../isabelle/bin/isabelle build -v -d ../.. ML_Utils</test>
</set>
</testsuite>

4
lib/Monad_WP/Datatype_Schematic.thy
View File

@ -6,8 +6,8 @@
theory Datatype_Schematic
imports
MLUtils
TermPatternAntiquote
ML_Utils.MLUtils
ML_Utils.TermPatternAntiquote
begin
text \<open>

2
lib/Monad_WP/wp/WP.thy
View File

@ -9,7 +9,7 @@ imports
WP_Pre
WPFix
Apply_Debug
MLUtils
ML_Utils.MLUtils
begin
definition

10
lib/ROOT
View File

@ -10,8 +10,8 @@ session Lib (lib) = Word_Lib +
sessions
"HOL-Library"
"HOL-Eisbach"
ML_Utils
directories
"ml-helpers"
"subgoal_focus"
"Monad_WP"
"Monad_WP/wp"
@ -49,14 +49,6 @@ session Lib (lib) = Word_Lib +
Apply_Debug
MonadicRewrite
HaskellLemmaBucket
"ml-helpers/MkTermAntiquote"
"ml-helpers/TermPatternAntiquote"
"ml-helpers/TacticAntiquotation"
"ml-helpers/MLUtils"
"ml-helpers/TacticTutorial"
"ml-helpers/MkTermAntiquote_Tests"
"ml-helpers/TacticAntiquotation_Test"
"ml-helpers/TermPatternAntiquote_Tests"
FP_Eval
"subgoal_focus/Subgoal_Methods"
Insulin

2
lib/RangeMap.thy
View File

@ -8,7 +8,7 @@ theory RangeMap
imports
FastMap
FP_Eval
MkTermAntiquote
ML_Utils.MkTermAntiquote
begin
text \<open>

5
lib/Trace_Schematic_Insts.thy
View File

@ -6,9 +6,8 @@
theory Trace_Schematic_Insts
imports
Main
MLUtils
TermPatternAntiquote
ML_Utils.MLUtils
ML_Utils.TermPatternAntiquote
begin
text \<open>