mkdir verification
cd verification
repo init -u ssh://[email protected]/seL4/verification-manifest.git
repo sync -m default.xml
docker run -v `pwd`:/work -w /work/l4v --rm -it trustworthysystems/l4v

rm -rf ~/.isabelle
mkdir -p ~/.isabelle/etc
cp -i misc/etc/settings ~/.isabelle/etc/settings
./isabelle/bin/isabelle components -a
./isabelle/bin/isabelle jedit -bf
./isabelle/bin/isabelle build -bv HOL
misc/regression/run_tests.py AutoCorresTest

root@ba717596fdbd:/work/l4v# misc/regression/run_tests.py AutoCorresTest
Running 4 test(s)...
  Started isabelle ...
  Finished isabelle                  FAILED *    ( 0:00:29 real,  0:01:52 cpu,  2.94GB)
  Finished CParser                   SKIPPED *
  Finished AutoCorres                SKIPPED *
  Finished AutoCorresTest            SKIPPED *

------------------------------------------------------------------------
TEST FAILED: isabelle

...
*** Failed to load theory "Word_Lib.Word_EqI" (unresolved "Word_Lib.More_Word", "Word_Lib.Traditional_Infix_Syntax")
*** Failed to load theory "Word_Lib.Most_significant_bit" (unresolved "Word_Lib.Bits_Int", "Word_Lib.Traditional_Infix_Syntax")
*** Failed to load theory "Word_Lib.Generic_set_bit" (unresolved "Word_Lib.Bits_Int", "Word_Lib.Most_significant_bit")
*** Failed to load theory "Word_Lib.Typedef_Morphisms" (unresolved "Word_Lib.Bits_Int")
*** Failed to load theory "Word_Lib.Aligned" (unresolved "Word_Lib.More_Word", "Word_Lib.Typedef_Morphisms", "Word_Lib.Word_EqI")
*** Failed to load theory "Word_Lib.Next_and_Prev" (unresolved "Word_Lib.Aligned")
*** Failed to load theory "Word_Lib.Word_Lemmas" (unresolved "Word_Lib.Aligned", "Word_Lib.Enumeration_Word", "Word_Lib.More_Word", "Word_Lib.Most_significant_bit")
*** Failed to load theory "Word_Lib.Word_8" (unresolved "Word_Lib.Enumeration_Word", "Word_Lib.More_Word", "Word_Lib.Word_Lemmas")
*** Failed to load theory "Word_Lib.Reversed_Bit_Lists" (unresolved "Word_Lib.Aligned", "Word_Lib.Least_significant_bit", "Word_Lib.Most_significant_bit", "Word_Lib.Typedef_Morphisms")
*** Failed to load theory "Word_Lib.Ancient_Numeral" (unresolved "Word_Lib.Reversed_Bit_Lists")
*** Failed to load theory "Word_Lib.Bitwise" (unresolved "Word_Lib.Reversed_Bit_Lists")
*** Failed to load theory "Word_Lib.Bitwise_Signed" (unresolved "Word_Lib.Bitwise")
*** Failed to load theory "Word_Lib.More_Word_Operations" (unresolved "Word_Lib.Aligned", "Word_Lib.Reversed_Bit_Lists")
*** Failed to load theory "Word_Lib.Word_32" (unresolved "Word_Lib.Bitwise", "Word_Lib.More_Word_Operations", "Word_Lib.Rsplit", "Word_Lib.Word_Lemmas", "Word_Lib.Word_Syntax")
*** Failed to load theory "Word_Lib.Word_Lemmas_Internal" (unresolved "Word_Lib.Many_More", "Word_Lib.More_Word_Operations", "Word_Lib.Word_Lemmas", "Word_Lib.Word_Syntax")
*** Failed to load theory "Word_Lib.Word_Lemmas_Prefix" (unresolved "Word_Lib.Word_Lemmas", "Word_Lib.Word_Lemmas_Internal")
*** Failed to load theory "Word_Lib.Word_Lib_Sumo" (unresolved "Word_Lib.Aligned", "Word_Lib.Ancient_Numeral", "Word_Lib.Bits_Int", "Word_Lib.Bitwise", "Word_Lib.Bitwise_Signed", "Word_Lib.Enumeration_Word", "Word_Lib.Generic_set_bit", "Word_Lib.Least_significant_bit", "Word_Lib.Legacy_Aliases", "Word_Lib.Many_More", "Word_Lib.More_Word_Operations", "Word_Lib.Most_significant_bit", "Word_Lib.Next_and_Prev", "Word_Lib.Norm_Words", "Word_Lib.Reversed_Bit_Lists", "Word_Lib.Rsplit", "Word_Lib.Strict_part_mono", "Word_Lib.Traditional_Infix_Syntax", "Word_Lib.Typedef_Morphisms", "Word_Lib.Word_16", "Word_Lib.Word_32", "Word_Lib.Word_8", "Word_Lib.Word_EqI", "Word_Lib.Word_Lemmas", "Word_Lib.Word_Lemmas_Internal", "Word_Lib.Word_Lemmas_Prefix", "Word_Lib.Word_Syntax")
*** Failed to load theory "Word_Lib.Word_Lemmas_32_Internal" (unresolved "Word_Lib.Word_Lib_Sumo")
*** Failed to load theory "Word_Lib.WordSetup" (unresolved "Word_Lib.Distinct_Prop", "Word_Lib.Word_Lemmas_32_Internal")
*** Type unification failed: Occurs check!
***
*** Type error in application: incompatible operand type
***
*** Operator:  (=) (w AND m AND m) :: ??'a ⇒ bool
*** Operand:   w AND m :: ??'b ⇒ ??'c ⇒ ??'a
***
*** At command "lemma" (line 39 of "/work/l4v/lib/Word_Lib/More_Word.thy")
*** Extra variables on rhs: "NOT"
*** The error(s) above occurred in definition:
*** "wordNOT x ≡ NOT x"
*** At command "abbreviation" (line 16 of "/work/l4v/lib/Word_Lib/Word_Syntax.thy")
*** Extra variables on rhs: "NOT"
*** The error(s) above occurred in definition:
*** "complement x ≡ NOT x"
*** At command "definition" (line 13 of "/work/l4v/lib/Word_Lib/Legacy_Aliases.thy")
Unfinished session(s): Word_Lib

Finished at Tue Mar 29 21:01:07 GMT 2022
0:00:27 elapsed time, 0:01:11 cpu time, factor 2.55

------------------------------------------------------------------------


0/4 tests succeeded.

Tests failed.