Re: [isabelle-dev] NEWS: isabelle jedit options
I just tried isabelle jedit -R HOL-UNITY assuming that it would build an auxiliary image for HOL-Auth, which is imported. It built HOL-Auth rather than HOL-UNITY_requirements(HOL-Auth) so things are pretty subtle here. A little more explanation would be valuable. Larry > On 6 Jun 2018, at 16:36, Makarius wrote: > > It could just mean that these examples don't need an auxiliary image. > > Take the first example from NEWS: > > isabelle jedit -R HOL-Number_Theory > > It produces an image > "HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also > the title line of Isabelle/jEdit. > > It also puts you into the ROOT entry for HOL-Number_Theory, so you can > directly explore its theories in the Prover IDE. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
On 06/06/18 16:19, Lawrence Paulson wrote: > > According to the NEWS entry, option -R builds an auxiliary logic image. I > tried this with a couple of examples and no images were built. According to > the manual, this option opens the ROOT entry. It does seem to do that, though > I'm not sure why this facility is needed. > It could just mean that these examples don't need an auxiliary image. Take the first example from NEWS: isabelle jedit -R HOL-Number_Theory It produces an image "HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also the title line of Isabelle/jEdit. It also puts you into the ROOT entry for HOL-Number_Theory, so you can directly explore its theories in the Prover IDE. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
> On 6 Jun 2018, at 12:43, Makarius wrote: > > On 06/06/18 12:45, Lawrence Paulson wrote: >> I saw them of course, but what do they do? > > These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I > have simplified and clarified the situation, updated NEWS and > documentation in the "jedit" manual. > > Right now the main question is if this is sufficient for the release, > and the documentation clear. Having tinkered with these things, read the NEWS entry and read the relevant section of the manual, I am still completely in the dark. According to the NEWS entry, option -R builds an auxiliary logic image. I tried this with a couple of examples and no images were built. According to the manual, this option opens the ROOT entry. It does seem to do that, though I'm not sure why this facility is needed. Surely it wouldn't be difficult to add a few lines of text, describing the sort of situation in which this option is useful. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
On 06/06/18 12:45, Lawrence Paulson wrote: > I saw them of course, but what do they do? These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I have simplified and clarified the situation, updated NEWS and documentation in the "jedit" manual. Right now the main question is if this is sufficient for the release, and the documentation clear. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
> Am 05.06.2018 um 23:01 schrieb Makarius : > > These options are very relevant for the coming release. I am interested > to get feedback from early adopters, if this is already sufficient or > requires further refinement. > > In other words, the question behind this: Can be get rid of most > auxiliary images in AFP (e.g. "Foo_Lib", "Pre_Foo")? I started to use -S HOL-ODE-Numerics and got rid of HOL-ODE-Refinement (which was such an auxiliary image) in AFP/cf739ca. -S is very helpful because it reduces the start-up time for Isabelle/jEdit (with the AFP in ROOTS) from 100s to 30s (compared to -R). I can also imagine that auxiliary images get outdated easily (importing too much or too little), and so it is good that -R/-S takes care of this potential maintenance efforts. Fabian 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
Re: [isabelle-dev] NEWS: isabelle jedit options
I saw them of course, but what do they do?
Larry
> On 5 Jun 2018, at 22:19, Makarius wrote:
>
> On 05/06/18 23:06, Lawrence Paulson wrote:
>> I’d find an example helpful, as your brief description is pretty cryptic.
>> Larry
>>
>>> On 5 Jun 2018, at 22:01, Makarius wrote:
>>>
>>> These options are very relevant for the coming release. I am interested
>>> to get feedback from early adopters, if this is already sufficient or
>>> requires further refinement.
>
> The NEWS contains these examples:
>
> Examples:
>isabelle jedit -R HOL-Number_Theory
>isabelle jedit -R HOL-Number_Theory -A HOL
>isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
>isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
>
> Here are more examples:
>
>isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Analysis
>isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Probability
>isabelle jedit -d '$AFP' -S Deep_Learning
>
> Alexander Bentkamp needs to be credited for writing a clear
> specification of the intermediate image Deep_Learning_Lib: {* Theories
> that are not part of HOL-Probability but are used by this entry *}.
>
> From there it was reasonably easy to implement the above options, but
> users need to start using them, and stop publishing old development
> artefacts in AFP.
>
>
> Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
On 05/06/18 23:06, Lawrence Paulson wrote:
> I’d find an example helpful, as your brief description is pretty cryptic.
> Larry
>
>> On 5 Jun 2018, at 22:01, Makarius wrote:
>>
>> These options are very relevant for the coming release. I am interested
>> to get feedback from early adopters, if this is already sufficient or
>> requires further refinement.
The NEWS contains these examples:
Examples:
isabelle jedit -R HOL-Number_Theory
isabelle jedit -R HOL-Number_Theory -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
Here are more examples:
isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Analysis
isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Probability
isabelle jedit -d '$AFP' -S Deep_Learning
Alexander Bentkamp needs to be credited for writing a clear
specification of the intermediate image Deep_Learning_Lib: {* Theories
that are not part of HOL-Probability but are used by this entry *}.
From there it was reasonably easy to implement the above options, but
users need to start using them, and stop publishing old development
artefacts in AFP.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
I’d find an example helpful, as your brief description is pretty cryptic. Larry > On 5 Jun 2018, at 22:01, Makarius wrote: > > These options are very relevant for the coming release. I am interested > to get feedback from early adopters, if this is already sufficient or > requires further refinement. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: isabelle jedit options
On 04/06/18 14:27, Makarius wrote: > *** Isabelle/jEdit Prover IDE *** > > * The command-line tool "isabelle jedit" provides more flexible options > for session management: > - option -R builds an auxiliary logic image with all required theories > from other sessions, relative to an ancestor session given by option > -A (default: parent) > - option -S is like -R, with a focus on the selected session and its > descendants (this reduces startup time for big projects like AFP) > > Examples: > isabelle jedit -R HOL-Number_Theory > isabelle jedit -R HOL-Number_Theory -A HOL > isabelle jedit -d '$AFP' -S Formal_SSA -A HOL > isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis > > > This refers to Isabelle/bcdc47c9d4af, it is a clarification and > simplification from earlier options. That changeset also contains the > updated documentation. These options are very relevant for the coming release. I am interested to get feedback from early adopters, if this is already sufficient or requires further refinement. In other words, the question behind this: Can be get rid of most auxiliary images in AFP (e.g. "Foo_Lib", "Pre_Foo")? Typically they just slow down the build process -- due to reduced parallelism and extra file-system operations to compact/store/load the intermediate image. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
