Re: [isabelle-dev] weird error message on startup

2017-12-07 Thread Lawrence Paulson 
I was able to fix the problem by going to the afp-devel directory and typing 
“hg fetch". I guess some big incompatible changes had taken place.
Larry

> On 6 Dec 2017, at 22:32, Makarius  wrote:
> 
> On 06/12/17 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?
> 
> It looks like you have an alien AFP version in your ROOTS or -d options,
> one that does not fit to the Isabelle version.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] weird error message on startup

2017-12-06 Thread Makarius 
On 06/12/17 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?

It looks like you have an alien AFP version in your ROOTS or -d options,
one that does not fit to the Isabelle version.


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] weird error message on startup

2017-12-06 Thread 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:
"\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:
"\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:

[isabelle-dev] weird error message on startup

2017-12-06 Thread Lawrence Paulson 
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:
"\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:
"\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