Re: [isabelle-dev] weird error message on startup
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] NEWS: antiquoted cartouches
On 05/12/17 17:18, Makarius wrote:
> *** Prover IDE -- Isabelle/Scala/jEdit ***
>
> * Named control symbols (without special Unicode rendering) are shown as
> bold-italic keyword. This is particularly useful for the short form of
> antiquotations with control symbol: \<^name>\argument\. The
> action
> "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
> arguments into this format.
>
>
> This refers to Isabelle/540eeaf88a63.
>
> Still required: update of various ML antiquotations to allow cartouche
> arguments. Right now it already works e.g. for @{typ}, @{term}, @{prop}.
Isabelle/909dcdec2122 enables many more ML antiquotations for this fancy
notation. Note that @{thm}, @{thms}, @{lemma} do not work due to their
more complex syntax.
Using action "isabelle.antiquoted_cartouche" in Isabelle/jEdit, I have
already updated all of src/Pure (dea94b1aabc3) and some of src/Tools and
src/HOL/Tools (e61557884799). Since there are so many ML sources, it is
probably better to upgrade the "isabelle update_cartouches" command-line
tool for this task.
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
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
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
Re: [isabelle-dev] NEWS: document_tags
On 05/12/2017 17:21, Makarius wrote:
*** Document preparation ***
* System option "document_tags" specifies a default for otherwise
untagged commands. This is occasionally useful to control the global
visibility of commands via session options (e.g. in ROOT).
* Document markup commands ('section', 'text' etc.) are implicitly
tagged as "document" and visible by default. This avoids the application
of option "document_tags" to these commands.
Thanks for this. Just a bit of context info: this simplifies the creation of
documents where only a few key parts of a theory are shown (eg main definitions
and thms). This in turn can be used to produce readable documentation for large
sessions (like HOL-Analysis).
Tobias
This refers to Isabelle/386a31d6d17a.
An example session is attached.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
