[isabelle-dev] weird error message on startup

[Tobias Nipkow]

I have modified HOL-Analysis but broke latex as a result. I have undone it again 
just now. No idea if this has anything to do with your problem.

Tobias

On 06/12/2017 15:48, Lawrence Paulson wrote:
> I've just updated to a recent version (fa1173288322) and tried to run a session by the following command:
> 
> isabelle jedit -l HOL-Analysis CV.thy
> 
> And then I get an alert box containing the appended text. Any idea what's going wrong here?
> 
> Larry
> 
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
> The error(s) above occurred for theory "Markov_Models.Probability"
> (required by "Markov_Models.Markov_Models" via "Markov_Models.Markov_Models_Auxiliary") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Markov_Models_Auxiliary.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
> The error(s) above occurred in session "Markov_Models" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/ROOT")
> [ line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_App.thy"] error: keyword "begin" expected,
> but string was found:
> "\<ge>t"
> 
> 
> ^
> The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_App"
> (required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy")
> [ line 15 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy"] error: keyword "begin" expected,
> but string was found:
> "\<ge>t"
> 
> 
> ^
> The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_Std"
> (required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via "Lambda_Free_KBOs.Lambda_Free_KBO_Basic") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Basic.thy")
> [ line 16 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy"] error: keyword "begin" expected,
> but string was found:
> ">p"
> 
> 
> ^
> The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs"
> (required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy")
> The error(s) above occurred in session "Lambda_Free_KBOs" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
> The error(s) above occurred for theory "MFMC_Countable.Probability"
> (required by "Probabilistic_While.While_SPMF" via "MFMC_Countable.Rel_PMF_Characterisation" via "MFMC_Countable.Matrix_For_Marginals" via "MFMC_Countable.MFMC_Misc") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/MFMC_Misc.thy")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy"
> The error(s) above occurred for theory "Probabilistic_While.Probability"
> (required by "Probabilistic_While.Bernoulli") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Bernoulli.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy"
> The error(s) above occurred in session "Probabilistic_While" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
> The error(s) above occurred for theory "Probabilistic_System_Zoo.Probability"
> (required by "Probabilistic_System_Zoo.Probabilistic_Hierarchy") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
> The error(s) above occurred in session "Probabilistic_System_Zoo" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy"
> The error(s) above occurred for theory "Randomised_Social_Choice.Probability"
> (required by "Randomised_Social_Choice.Randomised_Social_Choice" via "Randomised_Social_Choice.SDS_Lowering" via "Randomised_Social_Choice.Social_Decision_Schemes") (line 13 of "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Social_Decision_Schemes.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy"
> The error(s) above occurred in session "Randomised_Social_Choice" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy"
> The error(s) above occurred for theory "Quick_Sort_Cost.Probability"
> (required by "Quick_Sort_Cost.Randomised_Quick_Sort") (line 10 of "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy"
> The error(s) above occurred in session "Quick_Sort_Cost" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy"
> The error(s) above occurred for theory "Monad_Normalisation.Probability"
> (required by "CryptHOL.Misc_CryptHOL" via "Monad_Normalisation.Monad_Normalisation") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Monad_Normalisation.thy")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy"
> The error(s) above occurred for theory "Monomorphic_Monad.Probability"
> (required by "CryptHOL.Misc_CryptHOL" via "Monomorphic_Monad.Monomorphic_Monad") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy"
> The error(s) above occurred for theory "Applicative_Lifting.Probability"
> (required by "CryptHOL.SPMF_Applicative" via "Applicative_Lifting.Applicative_PMF") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Applicative_PMF.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy"
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy"
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy"
> The error(s) above occurred in session "CryptHOL" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/CryptHOL/ROOT")
> [ line 7 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/HF.thy"] error: keyword "begin" expected,
> but string was found:
> "~<:"
> 
> 
> ^
> The error(s) above occurred for theory "HereditarilyFinite.HF"
> (required by "Finite_Automata_HF.Finite_Automata_HF" via "HereditarilyFinite.Ordinal") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/Ordinal.thy")
> The error(s) above occurred in session "Finite_Automata_HF" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Finite_Automata_HF/ROOT")
> [ line 7 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/HF.thy"] error: keyword "begin" expected,
> but string was found:
> "~<:"
> 
> 
> ^
> The error(s) above occurred for theory "HereditarilyFinite.HF"
> (required by "HereditarilyFinite.Rank" via "HereditarilyFinite.Ordinal") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/Ordinal.thy")
> The error(s) above occurred in session "HereditarilyFinite" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/HereditarilyFinite/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy"
> The error(s) above occurred for theory "Monomorphic_Monad.Probability"
> (required by "Monomorphic_Monad.Monomorphic_Monad") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Monomorphic_Monad.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/Probability.thy"
> The error(s) above occurred in session "Monomorphic_Monad" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Monomorphic_Monad/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/Probability.thy"
> The error(s) above occurred for theory "Buffons_Needle.Probability"
> (required by "Buffons_Needle.Buffons_Needle") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/Buffons_Needle.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/Probability.thy"
> The error(s) above occurred in session "Buffons_Needle" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Buffons_Needle/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy"
> The error(s) above occurred for theory "Applicative_Lifting.Probability"
> (required by "Applicative_Lifting.Applicative_Functor" via "Applicative_Lifting.Applicative_PMF") (line 7 of "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Applicative_PMF.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/Probability.thy"
> The error(s) above occurred in session "Applicative_Lifting" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Applicative_Lifting/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/Probability.thy"
> The error(s) above occurred for theory "Density_Compiler.Probability"
> (required by "Density_Compiler.PDF_Transformations" via "Density_Compiler.Density_Predicates") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/Density_Predicates.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/Probability.thy"
> The error(s) above occurred in session "Density_Compiler" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Density_Compiler/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/Probability.thy"
> The error(s) above occurred for theory "Girth_Chromatic.Probability"
> (required by "Girth_Chromatic.Girth_Chromatic") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/Girth_Chromatic.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/Probability.thy"
> The error(s) above occurred in session "Girth_Chromatic" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Girth_Chromatic/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy"
> The error(s) above occurred for theory "Ergodic_Theory.Probability"
> (required by "Ergodic_Theory.SG_Library_Complement") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/SG_Library_Complement.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy"
> The error(s) above occurred in session "Ergodic_Theory" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy"
> The error(s) above occurred for theory "Ergodic_Theory.Probability"
> (required by "Lp.Functional_Spaces" via "Ergodic_Theory.SG_Library_Complement") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/SG_Library_Complement.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Ergodic_Theory/Probability.thy"
> The error(s) above occurred in session "Lp" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Lp/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/Probability.thy"
> The error(s) above occurred for theory "Random_Graph_Subgraph_Threshold.Probability"
> (required by "Random_Graph_Subgraph_Threshold.Subgraph_Threshold" via "Random_Graph_Subgraph_Threshold.Ugraph_Properties" via "Random_Graph_Subgraph_Threshold.Ugraph_Lemmas" via "Random_Graph_Subgraph_Threshold.Prob_Lemmas") (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/Probability.thy"
> The error(s) above occurred in session "Random_Graph_Subgraph_Threshold" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Random_Graph_Subgraph_Threshold/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
> The error(s) above occurred for theory "Markov_Models.Probability"
> (required by "Probabilistic_Noninterference.Interface" via "Markov_Models.Discrete_Time_Markov_Chain" via "Markov_Models.Markov_Models_Auxiliary") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Markov_Models_Auxiliary.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
> The error(s) above occurred in session "Probabilistic_Noninterference" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_Noninterference/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/Probability.thy"
> The error(s) above occurred for theory "Fisher_Yates.Probability"
> (required by "Fisher_Yates.Fisher_Yates") (line 11 of "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/Fisher_Yates.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/Probability.thy"
> The error(s) above occurred in session "Fisher_Yates" (line 2 of "/Users/lp15/isabelle/afp/devel/thys/Fisher_Yates/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/List_Update/Probability.thy"
> The error(s) above occurred for theory "List_Update.Probability"
> (required by "List_Update.Move_to_Front" via "List_Update.Competitive_Analysis" via "List_Update.Prob_Theory") (line 8 of "/Users/lp15/isabelle/afp/devel/thys/List_Update/Prob_Theory.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/List_Update/Probability.thy"
> The error(s) above occurred in session "List_Update" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/List_Update/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy"
> The error(s) above occurred for theory "Monad_Normalisation.Probability"
> (required by "Monad_Normalisation.Monad_Normalisation") (line 12 of "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Monad_Normalisation.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/Probability.thy"
> The error(s) above occurred in session "Monad_Normalisation" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Monad_Normalisation/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
> The error(s) above occurred for theory "Probabilistic_System_Zoo-Non_BNFs.Probability"
> (required by "Probabilistic_System_Zoo-Non_BNFs.Probabilistic_Hierarchy") (line 5 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
> The error(s) above occurred in session "Probabilistic_System_Zoo-Non_BNFs" (line 28 of "/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
> The error(s) above occurred for theory "MFMC_Countable.Probability"
> (required by "MFMC_Countable.Max_Flow_Min_Cut_Countable" via "MFMC_Countable.MFMC_Misc") (line 6 of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/MFMC_Misc.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
> The error(s) above occurred in session "MFMC_Countable" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/ROOT")
> [ line 12 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPO_App.thy"] error: keyword "begin" expected,
> but string was found:
> "\<ge>t"
> 
> 
> ^
> The error(s) above occurred for theory "Lambda_Free_RPOs.Lambda_Free_RPO_App"
> (required by "Lambda_Free_RPOs.Lambda_Free_RPOs") (line 11 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPOs.thy")
> [ line 14 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Std.thy"] error: keyword "begin" expected,
> but string was found:
> "\<ge>t"
> 
> 
> ^
> The error(s) above occurred for theory "Lambda_Free_RPOs.Lambda_Free_RPO_Std"
> (required by "Lambda_Free_RPOs.Lambda_Free_RPOs" via "Lambda_Free_RPOs.Lambda_Free_RPO_Optim") (line 9 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/Lambda_Free_RPO_Optim.thy")
> The error(s) above occurred in session "Lambda_Free_RPOs" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_RPOs/ROOT")
> Cannot load theory file "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/Probability.thy"
> The error(s) above occurred for theory "UpDown_Scheme.Probability"
> (required by "UpDown_Scheme.Grid_Point") (line 4 of "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/Grid_Point.thy")
> No such file: "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/Probability.thy"
> The error(s) above occurred in session "UpDown_Scheme" (line 3 of "/Users/lp15/isabelle/afp/devel/thys/UpDown_Scheme/ROOT")
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20171206/a03b2ba5/attachment.bin>