Hi Larry, I guess you have to update your local AFP clone also.
Hope this helps,
Florian
Am 25.04.2018 um 18:03 schrieb Lawrence Paulson:
> In the past couple of days, upon launching Isabelle jEdit, I get an alert box
> with the message above and the attached text. Any ideas?
>
> Larry
>
> ~/isabelle/Repos/src/Pure: hg id
> 362baebe25a5 tip
>
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Affine_Arithmetic.Affine_Arithmetic" via
> "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print")
> (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/Print.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "HOL-ODE-Refinement" (line 19 of
> "/Users/lp15/isabelle/afp/devel/thys/Ordinary_Differential_Equations/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "JinjaThreads.Basic_Main") (line 5 of
> "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/Basic/Basic_Main.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "JinjaThreads" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via
> "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via
> "CAVA_Base.Code_String") (line 9 of
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Maxflow_Lib" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Flow_Networks/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char" (line 14 of
> "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Iptables_Semantics" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "FOL_Harrison.FOL_Harrison") (line 14 of
> "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/FOL_Harrison.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "FOL_Harrison" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "LTL.LTL_Example") (line 9 of
> "/Users/lp15/isabelle/afp/devel/thys/LTL/example/LTL_Example.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "LTL" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/LTL/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "LLL_Factorization.Modern_Computer_Algebra_Problem") (line 13 of
> "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "LLL_Factorization" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Native_Word.Native_Cast") (line 8 of
> "/Users/lp15/isabelle/afp/devel/thys/Native_Word/Native_Cast.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Native_Word" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Native_Word/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via
> "CAVA_Base.Code_String") (line 9 of
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "CAVA_Base" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Transition_Systems_and_Automata.NBA_Explicit" via
> "Transition_Systems_and_Automata.NBA_Nodes" via
> "DFS_Framework.Reachable_Nodes" via "DFS_Framework.DFS_Framework" via
> "DFS_Framework.Param_DFS" via "CAVA_Base.CAVA_Base" via
> "CAVA_Base.CAVA_Code_Target" via "CAVA_Base.Code_String") (line 9 of
> "/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Transition_Systems_and_Automata"
> (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Transition_Systems_and_Automata/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Knuth_Morris_Pratt.KMP") (line 4 of
> "/Users/lp15/isabelle/afp/devel/thys/Knuth_Morris_Pratt/KMP.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Knuth_Morris_Pratt" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Knuth_Morris_Pratt/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Affine_Arithmetic.Affine_Arithmetic" via
> "Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print")
> (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/Print.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Affine_Arithmetic" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/ROOT")
> Cannot load theory "HOL-Library.Code_Char"
> The error(s) above occurred for theory "HOL-Library.Code_Char"
> (required by "Isabelle_Meta_Model.Parser_Pure" via
> "Isabelle_Meta_Model.Meta_Pure" via "Isabelle_Meta_Model.Init") (line 39 of
> "/Users/lp15/isabelle/afp/devel/thys/Isabelle_Meta_Model/Init.thy")
> No such file: "HOL-Library.Code_Char"
> The error(s) above occurred in session "Isabelle_Meta_Model" (line 3 of
> "/Users/lp15/isabelle/afp/devel/thys/Isabelle_Meta_Model/ROOT")
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
