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] OCaml 4.06.0 drops nums.cma
On 06/06/18 11:39, Lars Hupel wrote: >> The opam executables only require a few MB. The result in >> ~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair >> investment to evade the "dynamic version hell", and normal Isabelle >> users won't have to see it. >> >> So we could provide "isabelle opam" as wrapper for something like "opam >> --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle >> opam_init" for the specific compiler version setup. Our component wiring >> would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for the >> result. > > That sounds reasonable. What is the reason for placing "opam" under > "$ISABELLE_HOME_USER" (by default), though? I don't see a reason why > this couldn't be shared with an existing installation. I've misunderstood the "opam init --comp" procedure, with its tendency towards a single version. With "opam switch install" it is possible to install arbitrary (disjoint) versions, so indeed we can reuse the central ~/.opam root (with the minor disadvantage that it appears to assume just one OS platform, i.e. the HOME cannot be shared among platforms). > Would it be possible to specify the concrete compiler as a system > option? The big benefit there is that it would decrease maintenance > burden: session authors could select their "ocamlc" version in "options > [...]". It means people who have custom OCaml code printing (like Simon) > don't have to care about a hard-coded "4.05.0" somewhere; they'll get a > consistent setup regardless. In practice "their" version means a version in distant past that was the current one when the author was working on the session. I was more thinking of one standard OCaml version for a particular Isabelle version, which could be just ISABELLE_OCAML_VERSION in etc/settings. Multiple Isabelle versions can take this from a central ~/.opam store to produce ISABELLE_OCAML and ISABELLE_OCAMLC, but within each Isabelle version it should be a constant, not a variable. This conforms with the idea of Isabelle components: we include one fixed version for each tool, such that everything fits nicely together. 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 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] OCaml 4.06.0 drops nums.cma
> I have now experimented a bit with opam-1.2.2 on Linux, Mac OS X, > Windows/Cygwin64. It appears to work quite well, e.g. like this: > > ./opam-1.2.2-x86_64-Darwin init --root ~/.isabelle/opam --comp 4.05.0 > > The opam executables only require a few MB. The result in > ~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair > investment to evade the "dynamic version hell", and normal Isabelle > users won't have to see it. > > So we could provide "isabelle opam" as wrapper for something like "opam > --root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle > opam_init" for the specific compiler version setup. Our component wiring > would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for the > result. That sounds reasonable. What is the reason for placing "opam" under "$ISABELLE_HOME_USER" (by default), though? I don't see a reason why this couldn't be shared with an existing installation. Would it be possible to specify the concrete compiler as a system option? The big benefit there is that it would decrease maintenance burden: session authors could select their "ocamlc" version in "options [...]". It means people who have custom OCaml code printing (like Simon) don't have to care about a hard-coded "4.05.0" somewhere; they'll get a consistent setup regardless. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
