Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma
On 14/03/2019 20:03, Lars Hupel wrote: > > It initially failed because the OCaml people rely on "m4", which > apparently is not installed by default on modern Ubuntu systems. None of these ancient build tools are available by default on any current OS: m4, make, etc. are all evil in some sense. 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
On 14/03/2019 15:38, Lars Hupel wrote: >> I don't understand what is going on here. I thought I had to set >> ISABELLE_OCAML manually for this kind of code export to even do >> something. From what I can tell, I did /not/ set ISABELLE_OCAML on my >> machine, but I still get that error. Or did that behaviour change somehow? > > My understanding of the problem is as follows: Florian has thankfully > upgraded the code generator to emit code for OCaml 4.06+ with zarith. > However, it is still unclear how to install zarith systematically (i.e. > thread-safe but automatic). Where "automatic" means that a single Isabelle administrator (e.g. the local user) decides to invoke "isabelle ocaml_setup" and do other Isabelle administration in parallel. Afterwards the ISABELLE_OCAML settings will be correctly provided by the etc/settings scripts, without any further automatisms that can fail in strange ways. > For the error to be triggered I believe it is sufficient to have been > executed "isabelle opam_setup" once. This is not sufficient, and I have no time right now to look at the details. For the moment I have merely disabled Isabelle OPAM and OCaml as follows in $ISABELLE_HOME_USER/etc/settings: ISABELLE_OPAM_ROOT="" ISABELLE_OCAML="" ISABELLE_OCAMLC="" That is rather brutal, but allows me to continue with the current tip version. 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
On 13/03/2019 20:49, Florian Haftmann wrote: > Are there any issues remaining on this thread after > http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? I get this failure on my regular Ubuntu 18.04: *** Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Finite_Map") *** Code check failed for OCaml: "$ISABELLE_ROOT/lib/scripts/ocamlexec" ocamlfind ocamlopt -w pu -package zarith -linkpkg ROOT.ml *** At command "export_code" (line 1428 of "~~/src/HOL/Library/Finite_Map.thy") ocamlexec appears to reconfigure the OPAM installation insided Isabelle/ML, but this is conceptually wrong as I explained already. Also note that ISABELLE_OPAM_ROOT is always provided, even it that is not active. The general model is this: * Administrative tools like "isabelle ocaml_setup" or "isabelle ghc_setup" provide a local installation with sufficient information in the target directory, such that etc/settings can work out the resulting ISABELLE_OCAML / ISABELLE_OCAMLC or ISABELLE_GHC settings for the underlying platform, without running any installation tools again. * The Isabelle/ML world only refers to these settings as consolidated executables that don't change their own installation when invoked: many invocations will run in parallel. Moreover this must not assume that it is actually based on opam or stack: old-style manual installation of ocaml/ocamlc or ghc is still allowed (we've had this discussion some month ago concerning stack: it is just too heavy to be the only way to refer to ghc). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)
On 13/03/2019 21:06, Lars Hupel wrote: >> "Unable to increase stack" is one of the various messages that tells >> you that PolyML has run out of resources. It doesn't really tell you >> what the problem is though. It might be an actual problem or a >> temporary problem caused by a machine being overloaded. > > This is likely connected to the recent change of platform. I will > investigate this; maybe bumping the memory limit will resolve it. BTW, with Poly/ML 5.8 being official, you can avoid full x86_64 for most applications and always use the default x86_64_32. This saves a lot of resources: I usually have ML_OPTIONS="--minheap 1500" with an open upper end -- the implicit limit is approx. 16G. Even some entries of the slow/large groups of AFP work well with x86_64_32, but I usually throw them into on big x86_64 pot as a special case. Another remaining application of full x86_64 is the huge PIDE session forked by "isabelle dump" and related tools: it can require 64GB (excluding slow), and I have not explored the upper end yet. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
On 13/03/2019 21:12, Makarius wrote: > On 13/03/2019 21:00, Florian Haftmann wrote: >> Am 13.03.19 um 20:57 schrieb Lars Hupel: >>>> isabelle ocaml_opam install zarith >>> >>> This should ideally happen on-the-fly from within Isabelle/ML. >> >> Or maybe as implicit part of >> >> isabelle ocaml_setup > > Note that any change of the physical environment needs to happen in > administrative tools like "isabelle ocaml_setup": there is an implicit > assumption that there is only one administrator doing one thing at a > time. (E.g. in "isabelle build" and its physical update of heap and db > files.) > > In contrast, the parallel Isabelle/ML world cannot write to the global > file-system, without causing big problems. This requirement of statelessness also applies to the etc/settings shell scripts in the Isabelle components hierarchy. We have recently had tendencies to postulate automated build or download features here, but this is not going to work. There can be many simultaneous invocations of these scripts, and we cannot afford races, long-running operations, or spurious failures. Here is an example where I have amended such a mistake of mine, concerning Haskell stack: http://isabelle.in.tum.de/repos/isabelle/rev/c911716d29bb -- before there were spurious "stack" operations to access its stackage repository in uncontrolled ways. I've forgotten to apply the analogous change to the Isabelle/Naproche project (to be found on Github): it has already caused a lot of problems just with 2 developers and 3 users trying it out at Uni Bonn. I will have to revise "isabelle ghc_setup" further, to leave more accurate information in its installation directory (about platform-specific paths to ghc). Thus etc/settings can refer to that robustly and portably (note that even just different Linux installations may lead to different ghc installation names; of course it also needs to work with Windows and macOS on the same shared stack installation). Compared to that, "isabelle opam" is still lagging behing in various respects. I have myself no experience with the underlying opam tool, and it is also the old version 1.2.2 (which was imposed by Cygwin some months ago). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
On 13/03/2019 21:00, Florian Haftmann wrote: > Am 13.03.19 um 20:57 schrieb Lars Hupel: >>> isabelle ocaml_opam install zarith >> >> This should ideally happen on-the-fly from within Isabelle/ML. > > Or maybe as implicit part of > > isabelle ocaml_setup Note that any change of the physical environment needs to happen in administrative tools like "isabelle ocaml_setup": there is an implicit assumption that there is only one administrator doing one thing at a time. (E.g. in "isabelle build" and its physical update of heap and db files.) In contrast, the parallel Isabelle/ML world cannot write to the global file-system, without causing big problems. We have pending issues with AFP entries that violate this principle: maybe we manage to put it all into shape for the Isabelle2019 release, using stateless operations from Export/Generated_Files in ML for the 'codegen' command in particular. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Update to Poly/ML 5.8 -- and towards Isabelle2019
*** System *** * Update to Poly/ML 5.8 allows to use the native x86_64 platform without the full overhead of 64-bit values everywhere. This special x86_64_32 mode provides up to 16GB ML heap, while program code and stacks are allocated elsewhere. Thus approx. 5 times more memory is available for applications compared to old x86 mode (which is no longer used by Isabelle). The switch to the x86_64 CPU architecture also avoids compatibility problems with Linux and macOS, where 32-bit applications are gradually phased out. This refers to Isabelle/63721ee8c86c, it is now the official release of Poly/ML 5.8 by David Matthews. It all looks great so far, and there is still plenty of time for further testing until the official release of Isabelle2019. The present plan is to publish an unofficial Isabelle2019-RC0 snapshot in early April, and start officially with Isabelle2019-RC1 at the beginning of May. It all should be finalized an published until 15-Jun-2019, when I will go on travel (not vacation, but a visit to colleagues in Paris). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: option system_heaps
*** Isabelle/jEdit Prover IDE *** * Command-line options "-s" and "-u" of "isabelle jedit" override the default for system option "system_heaps" that determines the heap storage directory for "isabelle build". Option "-n" is now clearly separated from option "-s". *** System *** * The system option "system_heaps" determines where to store the session image of "isabelle build" (and other tools using that internally). Former option "-s" is superseded by option "-o system_heaps". INCOMPATIBILITY in command-line syntax. This refers to Isabelle/cc0b3e177b49. Short version: "isabelle build -s" is now "isabelle build -o system_heaps", and various other command-lines have been simplified. It is also possible to provide system_heaps via etc/preferences. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Creating Theorems in ML
On 28/02/2019 11:49, Achermann Reto wrote: > > [apologies in advance if this should have gone to the isabelle-users list] > > We are using ML in a project where we need to create a locale in HOL > from ML code. We managed to create the locale (local_theory) using > Expression.add_locale_cmd including any assumptions we defined in ML. Isabelle/ML belongs to the normal Isabelle user space, so isabelle-users is the place to go. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2
On 22/02/2019 22:59, Makarius wrote: > On 22/02/2019 16:47, Manuel Eberl wrote: >> I came upon a regrssion with the position information in terms that >> contain calligraphic or Fraktur letters, e.g.: >> >> theory Scratch >> imports Pure >> begin >> >> lemma "풜 풜 풜 풜 ()) a b c d e" >> >> The syntax error in this line is at the second closing parenthesis. In >> 3bfa28b3a5b2, Isabelle/jEdit displays the error at the space between "a" >> and "b". > > This is a problem introduced by Java 11: it works fine with Java 8. (I > will investigate it further later.) See now the following changes: changeset: 69840:a35033167f01 tag: tip user:wenzelm date:Sun Feb 24 13:00:43 2019 +0100 files: Admin/components/components.sha1 Admin/components/main description: updated to jedit_build-20190224 (new patches: favorites, glyphvector); changeset: 69839:828f3cd0dcf9 user:wenzelm date:Sun Feb 24 12:53:23 2019 +0100 files: src/Tools/jEdit/patches/glyphvector description: fallback on createGlyphVector for multi-character glyphs (e.g. 0x01d49c), as seen in Java 11; Java 11 correctly produces a complex glyph vector layout according to https://docs.oracle.com/en/java/javase/11/docs/api/java.desktop/java/awt/Font.html#layoutGlyphVector(java.awt.font.FontRenderContext,char[],int,int,int) but jEdit cannot handle that. So I made a fallback to something that is closer to the old behaviour in Java 8. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards Poly/ML 5.8
On 23/02/2019 11:45, Lars Hupel wrote: >> After a lot of refinements by David Matthews we are moving towards the >> new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a Poly/ML >> version of that number, without being official yet. The Isabelle NEWS >> already talk about an official release: > > Is it intentional that the system identifier is still 5.7.1? > > ML_SYSTEM=polyml-5.7.1 > > This also raises the question if that variable has any remaining uses. In 8c587dd44f51, I made some changes on two machines, but did not copy everything to the target, thus the etc/settings of the component is lagging behind. Right now ML_SYSTEM happens to have no meaning apart from some comment about the approximative version being used. Over the years it was sometimes used in conditional compilation and may get used like that at some point. Even ML_OPTIONS is less important these days that some years ago, because Isabelle/Scala provides most of the environment to the poly process. I did not change anything here, because build_history and the build_status database record the Poly/ML settings over many years, and I did not want to break the persistent data model just to be fully up-to-date at the "tip" version. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
On 23/02/2019 12:25, Lawrence Paulson wrote:
> Which reminds me: I define such abbreviations all the time, using “let”.
> Could let-abbreviations be folded upon printing?
>
>> On 23 Feb 2019, at 09:10, Manuel Eberl wrote:
>>
>> I for one almost always do
>>
>> define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
It might be better to introduce a proof-local version of 'abbreviation'.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2
On 22/02/2019 16:47, Manuel Eberl wrote: > I came upon a regrssion with the position information in terms that > contain calligraphic or Fraktur letters, e.g.: > > theory Scratch > imports Pure > begin > > lemma "풜 풜 풜 풜 ()) a b c d e" > > The syntax error in this line is at the second closing parenthesis. In > 3bfa28b3a5b2, Isabelle/jEdit displays the error at the space between "a" > and "b". Thanks for keeping an eye on isabelle-dev versions. This is a problem introduced by Java 11: it works fine with Java 8. (I will investigate it further later.) > Each "풜" seems to shift the offset > further, so I guess there's an off-by-one error in there somewhere. > Interestingly, not all letters cause this – e.g. "ℳ" seems to be fine. The calligraphic "A" belongs to a different Unicode standard than the calligraphc "M". E.g. see these results in Console / BeanShell or Console / Scala: > "풜".length() 2 > "ℳ".length() 1 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] infix line breaking
On 22/02/2019 17:20, Lawrence Paulson wrote: > The pretty printing of infix operators looks pretty terrible in the presence > of large terms. > > I’d like to propose having infix operators breaking at the start of the line > rather than at the end. Any thoughts? Recall this recent thread on that (and many other infix-related cans of worms): https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07670.html Changing arrangements from many decades ago always takes a bit longer than expected, and one needs to try hard to get a result that is significantly better than the status-quo. We have require 2 full release cycles just to get the relative simple reform of (+) and (*) through (with a fully convincing result). From my side, the following two reforms are on the top of the stack of further moves: (1) eliminate most (or all) ASCII replacement syntax with the help of the "isabelle update" tool, e.g. ":" vs. "\" (2) get ==> out of the infix topic for most practical purposes, by printing goal states in Isar notation (fixes/assumes/shows or fix/assume/show or show/if/for). For the coming release I merely see (1) happening really soon: the "isabelle update" tool belongs to certain newly introduced infrastructure that deserves proper consolidation. (It is time to start thinking about which already open threads should be closed for the release.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Towards Poly/ML 5.8
After a lot of refinements by David Matthews we are moving towards the new Poly/ML 5.8 release. Isabelle/8c587dd44f51 already bundles a Poly/ML version of that number, without being official yet. The Isabelle NEWS already talk about an official release: *** System *** * Poly/ML 5.8 allows to use the native x86_64 platform without the full overhead of 64-bit values everywhere. This special x86_64_32 mode provides up to 16GB ML heap, while program code and stacks are allocated elsewhere. Thus approx. 5 times more memory is available for applications compared to old x86 mode (which is no longer used by Isabelle). The switch to the x86_64 CPU architecture also avoids compatibility problems with Linux and macOS, where 32-bit applications are gradually phased out. This version also discontinues compatibility with Poly/ML 5.7.x, i.e. Isabelle2018 will not work with it, but polyml-test-8fda4fd22441 can still be used for that. I have also omitted old x86 from the bundle: it is difficult to build and run on current systems and much less stable than the new default x86_64_32. A minor disadvantage is that old hardware with only 4 GB will be somewhat slower, but we de-facto require 8 GB already. Everything in Isabelle + AFP should work with x86_64_32 on all platforms -- further automated and manual tests are running (some on old hardware with only 3 or 5 GB per CPU node, e.g. see https://isabelle.sketis.net/devel/build_status/AFP/index.html). Full x86_64 with 64-bit values/addresses is not required for anything in the visible universe of Isabelle + AFP. The "large" group runs considerably faster in full 64-bit mode, but this is not an existential problem for x86_64_32: a full "build -a" will be usually faster with x86_64_32 (and require much less resources). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] polyml-test-8fda4fd22441 available for testing
With Isabelle/ce4842d2d150 we are back to testing the forthcoming release of Poly/ML, with its special 32-in-64 bit mode for up to 16 GB ML heap memory. David Matthews has made several rounds of refinement, so there is some chance that spurious crashes have all disappeared. This needs to be tested thoroughly, of course. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 16/02/2019 14:07, Florian Haftmann wrote: > Am 14.02.19 um 13:34 schrieb Makarius: >> >> In contrast to my proposal concerning Flyspeck-Tame-Base it is better to >> keep the main AFP document unchanged, e.g. like this: >> >> session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... >> >> This will change the timing for Flyspeck-Tame in the recorded database, >> but such renamings occasionally happen over the years. > > See now > https://bitbucket.org/isa-afp/afp-devel/commits/00b771f6c60d99745fb933d4043c1ed123a427e5 Great. This looks fine to me. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 14/02/2019 12:04, Florian Haftmann wrote: >>> At the moment I am thinking whether the old approach of checking >>> everything except the computations can be restored without using fancy >>> low-level stuff. Maybe by a locale. >> >> This is indeed a bit fragile. I used to make manual tests of >> Flyspeck-Tame over some time, but now ignore that problem. >> >> Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base" >> that does everything except the actual "eval" steps, and postpone the >> checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ... > > Something like that indeed. A completeness proof relative to a locale > which has the computational results as assumption apt for later > interpretation. In contrast to my proposal concerning Flyspeck-Tame-Base it is better to keep the main AFP document unchanged, e.g. like this: session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... This will change the timing for Flyspeck-Tame in the recorded database, but such renamings occasionally happen over the years. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 14/02/2019 10:43, Florian Haftmann wrote: > > But https://isabelle.sketis.net/devel/build_status/ still indicates > failure for Flyspec-Tame from Wed 13th. Is there any chance that some > other non-termination proof requiring image_cong_simp [cong del] is > still left in Flyspeck-Tame? Maybe it is just a coincidence, it did work for Isabelle/18cb541a975f vs. AFP/9181c1974aa0, but later failed again for AFP/e064b4022c1c -- see also the "CSV" link on https://isabelle.sketis.net/devel/build_status Later today we should get new measurements. > Btw. that the ancient cond_eval hack has been replaced by a proper tag > has completely slipped out of my attention, hence I didn't notice that > Flyspeck-Tame is completely untested without very_slow. > > At the moment I am thinking whether the old approach of checking > everything except the computations can be restored without using fancy > low-level stuff. Maybe by a locale. This is indeed a bit fragile. I used to make manual tests of Flyspeck-Tame over some time, but now ignore that problem. Several days of unclear situation is a natural consequence of this arrangement. Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base" that does everything except the actual "eval" steps, and postpone the checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 10/02/2019 19:47, Makarius wrote: > I have fine-tuned the Isabelle DejaVu fonts in > Isabelle/4791988fcbc4 to impose the FreeType auto-hinting beforehand to > the TrueType file: this leads to isabelle_fonts-20190210 in > Isabelle/7e5a7a11d5d1. > > In summary: > > * Isabelle font rendering should be once again slightly better on Linux. > > * There is a small risk that it has slightly degraded on Windows and > macOS. > > In other words: early adopters should look closely if it is all fine. We > are (very slowly) moving towards the Isabelle2019 release (presumably > June 2019), and everything needs to be beyond doubt when released. I have invested 96 EUR into an old-style HD display from iiyama (1920x1080 21.5") and made some tests with Linux, Windows, macOS. * All platforms use the custom font-renderer of Java 11, not the native one (of Windows or macOS) as I first thought. * Using the defaults of Isabelle/f610115ca3d0, font shapes come out much better than in Java 8, 7, 6, and our "Isabelle DejaVu" fonts work nicely at 14, 16, 18, 24 pixels etc. -- in the past only 18 was OK, and most other sizes a bit too thin. * Some degree of blurriness appears to be normal for the FreeType font rendering of OpenJDK 11, but after a short time the Java 8 (Oracle) rendering already looks quite ugly to me. * Blurriness is absent on my up-to-date UHD display (330 EUR), even for tiny font sizes 14, 16, 18 -- normally I use 30 or 36. I cannot imagine anybody still using low resolution displays on a desk, after 5 years of fairly cheap UHD displays. Equipment that is used every day should be of good quality. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 10/02/2019 20:12, Makarius wrote: > On 10/02/2019 20:08, Peter Lammich wrote: >> No luck on my machine. The font rendering still looks slightly >> blurred. >> >> However, I'm using an old Linux (Ubuntu 16.04) ... may that be the >> reason? > > I don't think so, but you can make a quick test by booting current > Ubuntu 18.04 from an USB stick. The graphics drivers could make a > difference. I have briefly tried a USB stick of Ubuntu 16.04 on one of my test machines: as expected, it does not make a difference, i.e. the rendering quality is fairly good with the defaults of Isabelle/f610115ca3d0. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 10/02/2019 20:08, Peter Lammich wrote:
> No luck on my machine. The font rendering still looks slightly
> blurred.
>
> However, I'm using an old Linux (Ubuntu 16.04) ... may that be the
> reason?
I don't think so, but you can make a quick test by booting current
Ubuntu 18.04 from an USB stick. The graphics drivers could make a
difference.
Note that the jdk-11 distribution includes a copy of libfreetype.so, so
it appears to be reasonably self-contained in that respect. (I did not
read the relevant sources, because it is split between a Java and a
native part in C, and the latter sources always require extra work to
locate.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 05/02/2019 20:19, Makarius wrote: > On 05.02.19 11:43, Peter Lammich wrote: >> >> Is this worsening due to another Java version, due to the new Isabelle >> font, or has it some other reasons? How to find out? > > From a distance, I would say that this is a matter of the Java 11 > font-renderer, which is provided by https://adoptopenjdk.net. The one by > Oracle is much worse -- OpenJdk not the non-free Java. (Note that the > license change of non-free Oracle Java no longer allows to bundle it.) Even more, JDK 11 from Oracle is now distributed as non-free: users have to pay a subscription to use it in applications. Only some testing and development is allowed without extra payment. (See https://www.oracle.com/technetwork/java/javase/terms/license/javase-license.html). Java 8 is being phased out after Jan-2019. Since the Java community is notoriously slow in giving up legacy versions, there will be a bit more time to hold the breath and pretend that nothing has happened. In contrast, Isabelle is already on Java 11: it performs much better than Java 8, especially on high-end hardware with many cores (potentially also on "containers" like Docker). I have already seen some Isabelle/Scala scalability problems some months ago; luckily this has been resolved with Java 11. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 08/02/2019 10:03, Christian Sternagel wrote: > > I am glad to hear that others have the same experience, I thought my > eyes were going bad ;) > > But seriously, "buy a new screen" is not always possible. For example, > in the upcoming summer term I am teaching an Isabelle class at the > University of Innsbruck. In my experience (and I just reconfirmed this > for the room I will be teaching in), the projectors we have here a > typically rather old (and have low resolution, but that is a different > story). > > At the moment there is a palpable difference (font rendering crispness > wise) between using Isabelle2018 with projector (which I will do anyway > for my class) and some recent development version (sorry I didn't note > down what changeset I used for testing my setup). Classic JDK 8 from Oracle and OpenJDK 11 (e.g. from AdoptOpenJDK) are different in many ways, and it is definitely required to get used to the new look of font rendering. (For me Isabelle2018 already looks very strange.) With proper parameters -- in software and hardware -- fonts should come out better than before. First of all, sub-pixel rendering should be enabled, see this NEWS entry from Isabelle/f714114b0571 (25-Oct-2018): *** Isabelle/jEdit Prover IDE *** * Improved sub-pixel font rendering (especially on Linux), thanks to OpenJDK 11. (In Java 8, sub-pixel rendering made things worse.) Since that that NEWS entry is a bit too implicit, I have now changed the default to enable "Subpixel HRGB" always on all platforms (Isabelle/f610115ca3d0). I have checked my usual test machines for Windows and macOS, to see that it all looks fine. Secondly, I have done some more research on FreeType, the renderer used for OpenJDK on Linux. It appears that the DejaVu family gets some special treatment if it shows up under its original name, but not if it is a renamed copy. So I have fine-tuned the Isabelle DejaVu fonts in Isabelle/4791988fcbc4 to impose the FreeType auto-hinting beforehand to the TrueType file: this leads to isabelle_fonts-20190210 in Isabelle/7e5a7a11d5d1. In summary: * Isabelle font rendering should be once again slightly better on Linux. * There is a small risk that it has slightly degraded on Windows and macOS. In other words: early adopters should look closely if it is all fine. We are (very slowly) moving towards the Isabelle2019 release (presumably June 2019), and everything needs to be beyond doubt when released. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 04/02/2019 14:17, Makarius wrote: > On 04/02/2019 10:37, Lars Hupel wrote: >> Is this related to the latest Poly/ML changes? The "slow" job still runs >> on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware >> is 8-core LRZ VM. > > I can confirm this: see > https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html > > I have switched back to stable polyml-5.7.1-8 for now (see > Isabelle/a5732629cc46) and will be unavailable for the next few days. This did not change the non-termination, but the following helps: changeset: 10116:9181c1974aa0 tag: tip user:wenzelm date:Sun Feb 10 16:49:10 2019 +0100 files: thys/Flyspeck-Tame/PlaneGraphIso.thy description: adapted to Isabelle/7e4966eaf781 -- avoid non-termination; changeset: 69777:7e4966eaf781 parent: 69767:d10fafeb93c0 user:haftmann date:Thu Jan 31 13:08:59 2019 + files: NEWS src/HOL/Analysis/Caratheodory.thy src/HOL/Analysis/Convex.thy src/HOL/Analysis/Elementary_Topology.thy src/HOL/Analysis/Embed_Measure.thy src/HOL/Analysis/Homotopy.thy src/HOL/Analysis/Sigma_Algebra.thy src/HOL/Binomial.thy src/HOL/Complete_Lattices.thy src/HOL/Enum.thy src/HOL/Fun.thy src/HOL/GCD.thy src/HOL/Hilbert_Choice.thy src/HOL/Hoare_Parallel/RG_Examples.thy src/HOL/Probability/ex/Dining_Cryptographers.thy src/HOL/Set.thy src/HOL/Set_Interval.thy src/HOL/UNITY/Comp/Alloc.thy description: proper congruence rule for image operator I have merely applied the recommendation from the NEWS: INCOMPATIBILITY; consider using declare image_cong_simp [cong del] in extreme situations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 05.02.19 20:19, Makarius wrote: From a distance, I would say that this is a matter of the Java 11 font-renderer, which is provided by https://adoptopenjdk.net. The one by Oracle is much worse -- OpenJdk not the non-free Java. (Note that the license change of non-free Oracle Java no longer allows to bundle it.) For completeness, this is how to experiment with different versions of JDK, e.g. the one that Ubuntu 18.04 provides as the "openjdk-11" package family: ISABELLE_JDK_HOME="/usr/lib/jvm/java-11-openjdk-amd64" in $ISABELLE_HOME_USER/etc/settings as usual. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font
On 05.02.19 11:43, Peter Lammich wrote: I just updated my Isabelle devel version (now on d21789843f01), and immediately noticed that the displayed fonts are significantly blurry. Find attached a side-by-side comparison of Isabelle-d21789843f01 (left) and Isabelle-2018 (right). At least on my monitor, the font display on the left side is significantly worse (blurred). Both use font size 18 with standard anti-aliasing method. Is this worsening due to another Java version, due to the new Isabelle font, or has it some other reasons? How to find out? From a distance, I would say that this is a matter of the Java 11 font-renderer, which is provided by https://adoptopenjdk.net. The one by Oracle is much worse -- OpenJdk not the non-free Java. (Note that the license change of non-free Oracle Java no longer allows to bundle it.) You can find out yourself by trying the IsabelleText font that is distributed with Isabelle2018: the ttf files need to go into ~/.fonts on Ubuntu; or elsewhere on other systems. It is important to remove the fonts after the experiment! Generally, the new fonts should be slightly better than before: the quality should be that of the original Deja Vu fonts without any censorship. I merely trim it to a well-defined collection of glyphs and add our Isabelle math symbols from the TeX family -- see "isabelle build_fonts" (e.g. in Isabelle/2c3e5e58d93f). > How to fix it? You know already that "fix" and "bug" is not in my vocabulary -- I don't use such street language. On up-to-date UHD displays the quality should of the new Java 11 + new fonts should be higher than ever before, so you can improve your overall situation by getting a new display. My huge UHD display at home was actually quite cheap: approx. 350 EUR. I do see the slight blurring on my ancient HD Sony Vaio from 2013, but I am not using that very often. Buying a new laptop is certainly more expensive than just a display -- nonetheless I am surprised how many 100 EUR displays are still standing on desks and stared at every day. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 05.02.19 13:18, Salomon Sickert wrote:
It should be easy to make this part of the formal session, with some
options [condition = ISABELLE_MLTON].
The 'export_code' command will have to emit generated files
(Generated_Files.add_files) to make the assembly work in Isabelle/ML.
I have already added support for executable exports in
Isabelle/c175499a7537 -- a few more such fine-tunings might be required.
Could someone point me to an example on how to do compilation with either mlton
or polyml within a formal session?
The build scripts in these two entries are copying the style of the CAVA entry
at that time and I’m not sure about the current best practices here.
A partial example with generated files is src/Tools/Haskell/Test.thy
(e.g. in Isabelle/2c3e5e58d93f): the generated Haskell sources are used
for a test build, but its result is thrown away instead of exporting it.
I have some ideas in the pipeline to make the 'export_files'
specifications in session ROOT entries more robust (no export by
default) and more useful (collective export on something like "isabelle
build -e").
We also need to wait for Florian Haftmann to provide the
Generated_Files.add_files facility to 'export_code' -- in parallel to
its existing Export.export. The main difference that this will be an
update on the theory.
(Note that I am presently busy elsewhere and only sporadically connected.)
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 01/02/2019 15:30, Lars Hupel wrote: > > – Sturm_Sequences produces some extra LaTeX documentation. The generated > PDF is even committed to the AFP. > >> * no generated files in the repository (these are not sources but >> results from sources) See now changeset: 10104:394951259923 user:wenzelm date:Mon Feb 04 16:42:52 2019 +0100 files: thys/Sturm_Sequences/ROOT thys/Sturm_Sequences/document/build thys/Sturm_Sequences/document/root_userguide.tex thys/Sturm_Sequences/guide/Makefile thys/Sturm_Sequences/guide/guide.pdf thys/Sturm_Sequences/guide/guide.tex thys/Sturm_Sequences/guide/isabelle.eps thys/Sturm_Sequences/guide/isabelle.pdf description: proper Isabelle document setup, without generated files in the repository; It means that the document will also show up in the generated HTML, similar to the userguide in AFP/Collections. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 04/02/2019 08:00, Salomon Sickert wrote: > > > To add a couple more to the list: > > — LTL has includes a parser that is used in an example and built using > LTL/examples/build_poly.sh > > — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh > and LTL_to_DRA/Code/build_mlton.sh It should be easy to make this part of the formal session, with some options [condition = ISABELLE_MLTON]. The 'export_code' command will have to emit generated files (Generated_Files.add_files) to make the assembly work in Isabelle/ML. I have already added support for executable exports in Isabelle/c175499a7537 -- a few more such fine-tunings might be required. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Uniform Isabelle repository clones via https://isabelle.sketis.net/repos
https://isabelle.sketis.net/repos provides uniform repository clones of Isabelle + AFP -- this is updated via cron + ssh every 10min. The original motivation was to avoid recurrent oddities with https certificates from other repository servers, with the most recent incident for Bitbucket (Isabelle/60b5a4731695): ERROR abort: api.media.atlassian.com certificate error: certificate is for dentalsaglik.com There is another benefit for direct browsing: just one uniform HTML view of repository content, using a current theme provided by Mercurial itself. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Timeouts in Flyspeck_Tame
On 04/02/2019 10:37, Lars Hupel wrote: > Is this related to the latest Poly/ML changes? The "slow" job still runs > on the x86_64 platform. Last time it worked was 76fbd806ebc5. Hardware > is 8-core LRZ VM. I can confirm this: see https://isabelle.sketis.net/devel/build_status/AFP_bulky_64bit_6_threads/index.html I have switched back to stable polyml-5.7.1-8 for now (see Isabelle/a5732629cc46) and will be unavailable for the next few days. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 15:37, Lawrence Paulson wrote: > This worked — thanks! > >> On 2 Feb 2019, at 13:56, Makarius wrote: >> >> Can you try the following in your $ISABELLE_HOME_USER/etc/settings? >> >> init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" OK. With Isabelle/76f2d492627e this is the default, and it is better to remove the init_component from local etc/settings again, to participate in further updates of the default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 14:56, Makarius wrote: > On 02/02/2019 14:39, Lawrence Paulson wrote: >> It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle >> jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. >> >> The reason I fetched in the first place was that I was getting crashes in my >> interactive sessions. > > Can you try the following in your $ISABELLE_HOME_USER/etc/settings? > > init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" > > Apparently, the last two updates on polyml-test were not as monotonic as > I was hoping, despite clear improvements by David Matthews. > > After a standard test, I will probably make the above version the > default again. I've done that now in Isabelle/dde776d1defa, after successful "isabelle build -a". Thus we are at least back to the status-quo from some days ago, where nobody noticed everyday crashes. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 02/02/2019 14:13, Florian Haftmann wrote: > * The module naming schema gets more sophisticated: default, name or > prefix. The key point is that this naming schema is again > target-language specific. Just abstractly, a reform should strive for unification and simplification whenever possible. The different languages have slightly different side-conditions, but maybe they can still be unified: e.g. the main NAME could become NAME.EXT or NAME/ depending on the situation. One could also use the const names to produce a default, e.g. according to the traditional scheme to concatenate const base names with "_" as separator. > This should cover all application cases. When export_code emits Generated_Files.add_files, there is always a possibility to do special-purpose Isabelle/ML programming with Generated_Files.get_files. No need to have all odd cases in one Isar command. > At the moment I am still in favour of a diagnostic command to emit sth > ad-hoc into the file system -- but this could be something separate from > export_code and maybe just use $ISABELLE_TMP_PREFIX/… as destination. For diagnostics I have used the "isabelle-export:" VFS in Isabelle/jEdit so far: if a physical file is required, it can be written from the editor (which actually cased the crash before Isabelle/9fd395ff57bc). Minor disadvantage: writing directory content is inconvenient. In that case there is also Generated_Files.write_files. Some months ago I've seen odd crashes with files written to $ISABELLE_TMP_PREFIX/ in Isabelle/ML and read in Isabelle/Scala. Moreover I've seen crashes of the Headless PIDE session of export_code with $ISABELLE_TMP_PREFIX in particular. There might be something wrong in my areas of responsibility, or something inherently fragile in concurrent access to a Unix file-system. These incidents motivated to revive the pending thread to eliminate physical files from export_code in the first place. Mathematical files in the theory context are more reliably than physical ones on a magnetic drum. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Analysis not building
On 02/02/2019 14:39, Lawrence Paulson wrote: > It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle > jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”. > > The reason I fetched in the first place was that I was getting crashes in my > interactive sessions. Can you try the following in your $ISABELLE_HOME_USER/etc/settings? init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202" Apparently, the last two updates on polyml-test were not as monotonic as I was hoping, despite clear improvements by David Matthews. After a standard test, I will probably make the above version the default again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] polyml-test-b68438d33c69
With Isabelle/76f2d492627e we are on polyml-test-b68438d33c69: it is
already fairly stable, but there are still some sporadic crashes,
notably on slow machines (e.g. for "isabelle build HOL" on lxbroy10 or
my macMini at home). On high-end machines, I can build all of Isabelle +
AFP without problems.
We do continue monotonically towards a stable Poly/ML version: David
Matthews has already sorted out various subtle issues on
https://github.com/polyml/polyml/commits/master -- leading up to current
b68438d33c69.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 01/02/2019 16:40, Lars Hupel wrote: >> The standard approach for the latter is to have the other tool directly >> import its source format into the theory context within Isabelle/ML, >> without the intermediate theory source. Doing this carefully, would even >> produce nice PIDE markup for the original sources. PIDE is an IDE for >> arbitrary user-defined languages. >> >> It might be worth doing this for tools like Lem eventually, but I have >> not looked at it closely so far. > > Lem is implemented in OCaml, so this seems like a stretch. I'd say > importing HOL4 into Isabelle is a more plausible solution. Yes, the motivation behind using Lem is diminished by the promising work of Fabian Immler. In general, though, alien tool output can be imported into the formal context. One merely needs to devise some tricks. A tool implemented in Haskell or OCaml should be particularly easy. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources
On 31/01/2019 23:11, Makarius wrote: > *** Isabelle/jEdit Prover IDE *** > > * The jEdit File Browser is more prominent in the default GUI layout of > Isabelle/jEdit: various virtual file-systems provide access to Isabelle > resources, notably via "favorites:" (or "Edit Favorites"). I have now reverted the default to "buffer" instead of "favorites", see changeset: 69781:a7529ac9c1c5 user:wenzelm date:Fri Feb 01 15:02:36 2019 +0100 files: src/Tools/jEdit/src/jEdit.props description: clarified default (amending ca9780325a21): it also affects "open-file" dialog, which should be "buffer"; The favorites are very important, but many long-term users still don't know about them. I need to find another way to make them easily accessible. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 01/02/2019 15:30, Lars Hupel wrote: > >> * no generated files in the repository (these are not sources but >> results from sources) > > What about generated theory files? This also affects the CakeML entry. I > could easily package Lem as a component, but how would "isabelle build" > call it? The present reform is mainly about generated output files, not input theory files. The standard approach for the latter is to have the other tool directly import its source format into the theory context within Isabelle/ML, without the intermediate theory source. Doing this carefully, would even produce nice PIDE markup for the original sources. PIDE is an IDE for arbitrary user-defined languages. It might be worth doing this for tools like Lem eventually, but I have not looked at it closely so far. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 01/02/2019 14:29, Lars Hupel wrote: >> In 2012 we eliminated all Makefiles from AFP: I did not know that some >> came back, or chose to ignore it. > > ~/work/afp (default)$ find thys/ -name Makefile > thys/Buchi_Complementation/code/Makefile > thys/Formal_SSA/Makefile > thys/LightweightJava/ott-src/Makefile > thys/Sturm_Sequences/guide/Makefile What are the remaining uses of these? How much of this can be integrated into the formal Isabelle session? How much of it is actually obsolete? We have plenty of mechanisms in "isabelle build" (and "isabelle process") that are waiting to be put into proper use. >From a maintenance point of view the goals are: * no generated files in the repository (these are not sources but results from sources) * no violations of the stateless PIDE model, e.g. commands that leave a trace of garbage in the natural environment while editing (such as "export_code ... file ..." with varying file names). In principle, everything should work on a read-only file-system. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 01/02/2019 12:43, Lars Hupel wrote: > > It would like to reiterate that the technical part of this issue is the > easy bit. The difficult bit is deciding policy: Should Isabelle > committers be responsible for breakage in downstream artifacts? In other > words, should the AFP stability guarantees be extended? Right now we > have that odd situation where extra sources are present (e.g. Makefiles) > but nobody bothers to look at them. In 2012 we eliminated all Makefiles from AFP: I did not know that some came back, or chose to ignore it. The formal status of sessions is defined via "isabelle build" -- that is a powerful tool that can do many things. I.e. we can easily define that anything outside of it as outside of AFP. As usual, the empirical proof of this claims works by going through the applications seen in practice, and to reform them to make them fit to the model. (This sometimes requires minor adjustments of the model.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources
On 31/01/2019 23:11, Makarius wrote: > *** Isabelle/jEdit Prover IDE *** > > * The jEdit File Browser is more prominent in the default GUI layout of > Isabelle/jEdit: various virtual file-systems provide access to Isabelle > resources, notably via "favorites:" (or "Edit Favorites"). There is an old oddity in "Edit Favorites" that I have now addressed here: changeset: 69779:a2218981a5d6 user:wenzelm date:Thu Jan 31 22:02:50 2019 +0100 files: src/Tools/jEdit/patches/favorites description: more accurate _listFiles -- avoid infinite infinite expansion of e.g. "$ISABELLE_HOME"; This minor change is not yet active: a future update of the jedit_build component will include it. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources
*** Isabelle/jEdit Prover IDE *** * The jEdit File Browser is more prominent in the default GUI layout of Isabelle/jEdit: various virtual file-systems provide access to Isabelle resources, notably via "favorites:" (or "Edit Favorites"). * Action "isabelle-export-browser" points the File Browser to the theory exports of the current buffer, based on the "isabelle-export:" virtual file-system. The directory view needs to be reloaded manually to follow ongoing document processing. * Action "isabelle-session-browser" points the File Browser to session information, based on the "isabelle-session:" virtual file-system. Its entries are structured according to chapter / session names, the open operation is redirected to the session ROOT file. This refers to Isabelle/b9a5805d1d70. I have also change the default GUI layout: global overview LEFT (Documentation, File Browser), local document information RIGHT (Theories, SideKick etc.) Output and interaction at the BOTTOM, as before. Within the repository I cannot impose arbitrary jEdit properties on a local settings directory, so it might require manual tinkering to imitate the default. (I usually rename $ISABELLE_HOME_USER/jedit temporarily to see the difference.) The "isabelle-session:" virtual file-system is the start of more serious access to Isabelle resources: right now it merely shows chapter/session tree structure, and opens the corresponding ROOT entry. Since the latter is also under PIDE control, CTRL/COMMAND-MOUSE-HOVER-CLICK quickly leads to some theories. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: option "jedit_text_overview"
*** Isabelle/jEdit Prover IDE ***
* System option "jedit_text_overview" allows to disable the text
overview column.
This refers to Isabelle/5a8ae7a4b7d0 -- it is a minor visual enhancement
for situations where the editor screen should look like a presentation,
without any distractions by extra GUI elements. (All other GUI elements
had already options in jEdit or Isabelle).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 31/01/2019 20:37, Mathias Fleury wrote: > >> On 31. Jan 2019, at 20:10, Makarius > >> Can you point to these special applications? >> >> If export_code uses Generated_Files.add_files (in addition to >> Export.export) we get both a check for unique names and an easy way to >> retrieve the exports in Isabelle/ML, e.g. to write to a temporary >> directory and do some tests. > > Can you give some more details on how to achieve this? > > Concrete application: I have a verified SAT solver (lets call that > function isasat), an unverified parser, and several large CNF files > (each one is several MB large). I would like to compile the SAT solver > with MLton*, test it on those CNF files. With some timings information > to identify regression if possible. > >> So far I have never seen an application that could not be made stateless >> and thus fit properly into the PIDE model. The general principle is to keep generated material inside the theory context (Generated_Files) and take them from there to produce other artifacts in Isabelle/ML, e.g. as a "sink" to produce error information, timing etc. It is also possible to formally export sources or artifacts to the session build database using Export.export: Isabelle/Scala can take results from there and do something else with it, but inside the build process, only after it. * Here is a simple example with 'generated_file': https://isabelle.in.tum.de/repos/isabelle/file/7e4966eaf781/src/Tools/Haskell/Haskell.thy * Here is a test build inside Isabelle/ML -- this is stateless thanks to a temp dir: https://isabelle.in.tum.de/repos/isabelle/file/7e4966eaf781/src/Tools/Haskell/Test.thy * Here is the use of the same sources in session database exports, written to a global file-space that is not the Isabelle (or AFP) repository: https://github.com/Naproche/Naproche-SAD/commit/698527fc6a47839bd48c521beb3d71129e3924a4 Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 31/01/2019 18:27, Peter Lammich wrote: > On Do, 2019-01-31 at 16:03 +0100, Makarius wrote: >> I have looked around at typical uses of 'export_code' in AFP. Most of >> the time it is just informative: writing a file and looking at it in >> the >> editor (or via the command-line!?), or doing that on the output >> channel. >> The isabelle-export: file-system covers that already, i.e. we should >> be >> able to eliminate almost all generated files from the AFP repository. >> >> So "export_code .. file" should just disappear -- it is semantically >> illtyped in PIDE: editing the "file" argument will leave a trace of >> machine oil spilled to the physical file-system. > > The problem here is actually deeper: > Many AFP-entries are designed to export code which then works together > with some external code. However, there seems to be no way to test > whether this external code works with the generated code. Can you point to these special applications? If export_code uses Generated_Files.add_files (in addition to Export.export) we get both a check for unique names and an easy way to retrieve the exports in Isabelle/ML, e.g. to write to a temporary directory and do some tests. So far I have never seen an application that could not be made stateless and thus fit properly into the PIDE model. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 14/01/2019 20:20, Florian Haftmann wrote:
>
>> * Are there remaining uses of 'file' with empty name? Is the virtual
>> file-system browser sufficiently convenient to inspect results
>> interactively?
>
> I checked the file system browser and would be quite content with it; as
> a bonus you can then make use of the syntax highlighting of jEdit (OCaml
> seems not be built-in, though).
>
> But I want to excite more feedback of users.
Here is some feedback from myself as a user: the new stateless model to
generate files works well, in particular the file-browser of
Isabelle/jEdit helps.
There was only a technical problem it that should no longer occur in
practice, see
changeset: 69696:9fd395ff57bc
user:wenzelm
date:Sun Jan 20 21:26:15 2019 +0100
files: Admin/components/components.sha1 Admin/components/main
src/Tools/jEdit/patches/vfs_manager
description:
avoid crash of jEdit.closeBuffer() via
TaskManager.instance.waitForIoTasks() due to race condition of save()
vs. automatic load() of already open buffer, e.g. relevant for save-as
on "isabelle-export:" artifacts;
In the mainstream this would probably be called a "fix", but the
conceptual problem behind it is still there: there are concurrent tasks
that are just concatenated in sequence, without taking the nesting of
the program structure into account. Proper futures are required instead
of slightly odd wait operations.
>> * How to specify proper (unique) export names: PIDE still lacks a
>> check for uniqueness of export names, but overwriting existing exports
>> is considered illegal. The 'file' allowed to produce separate names in
>> the past, but it has a different meaning now (and is a candidate for
>> deletion).
>
> Well, if we re-consider the syntax, we will also find a way for this.
>
>> Maybe 'export_code' should be renovated replaced by reformed commands
>> like this:
>>
>> * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is
>> optional and the default something like "generated" or "code". This
>> could be a "thy_decl" command that updates the theory context by
>> generated files that are accessible in Isabelle/ML, in addition to the
>> export; it would also include a check for duplicate names.
>>
>> * "code_checking CONSTS in LANGUAGE" -- observing that "export_code
>> ... checking" is actually a different command. It would be a "diag"
>> command as before (this is relevant for parallelism).
>
> Maybe the »checking« should just be a variant of the regular export.
>
> Hence the modification could be quite conservative:
>
> export_code CONSTS in LANGUAGE ( '(' OPTIONS ')' ) ( module_name NAME )
> ( file … | ( prefix … ) ( checked ) )
>
> where »file« denotes a relative root in the file system and »checked«
> indicated that the generated code will be checked implicitly.
I have looked around at typical uses of 'export_code' in AFP. Most of
the time it is just informative: writing a file and looking at it in the
editor (or via the command-line!?), or doing that on the output channel.
The isabelle-export: file-system covers that already, i.e. we should be
able to eliminate almost all generated files from the AFP repository.
So "export_code .. file" should just disappear -- it is semantically
illtyped in PIDE: editing the "file" argument will leave a trace of
machine oil spilled to the physical file-system.
We do need an explicit prefix and an internal check for duplicates, e.g.
as in the command 'generated_file'.
That should be really just a prefix for the exported artifact, not the
name itself: each language processor should be smart enough to derive
file or directory names from it as required. Thus the prefix locally
belongs in front of the arguments.
Here is an example from AFP/160ac13cdc05
SATSolverVerification/SatSolverCode.thy:
export_code solve
in OCaml file "code/solve.ML"
in SML file "code/solve.ocaml
in Haskell file "code/"
It could be turned into something like this:
export_code "code/" = solve in OCaml SML Haskell
Some details about the automatic name derivation scheme still need to be
sorted out -- or 'file' remains as an option to specify the suffix for
effective name (without writing anything to the file-system).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Afterthoughts on Local_Theory.subtarget_result
On 22/01/2019 22:24, Florian Haftmann wrote: > > as of 82f57315cade (followed-up by AFP bf62184), the still occasionally > seen Local_Theory.reset invocations are gone, conveniently replaced by > Local_Theory.subtarget_result. This looks clean and canonical. At least we have Local_Theory.reset out of the way in visible Isabelle/ML tool implementations: it is still present inside Local_Theory.close_target, though. I wonder what happens when that is removed: presumably it requires a lot of fine-tuning to make everything work again without that hidden reset. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Question about testing isabelle with Poly/ML x86_64_32
On 29/01/2019 16:14, João Rafael Nicola wrote: > > I've been using Isabelle/2018 in x86 (32) mode on a Xeon E3-1505M > (2.80GHz, 3.6Ghz turbo) 4-core, 64GB machine. Since I run frequently > into timeouts while running sledgehammer, proof methods > (metis,meson,etc.) or processing notation-heavy locales, I would like to > know how can I determine whether or not a shift to x86_64_32 would help. > How can I determine if the limited heap size of x86_32 Poly/ML might be > hindering Isabelle? Isabelle/jEdit has a "Monitor" panel, its "Heap" tab might provide some clues. The current test version of Poly/ML is polyml-test-1b2dcf8f5202. If you keep an eye on changing versions of https://isabelle.in.tum.de/repos/isabelle/file/tip/Admin/components/main you will see what is the latest and greatest one. Note that we still have 1 or 2 hard crash situations that need to be sorted out. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 25/01/2019 20:29, Bertram Felgenhauer wrote: > > - While most heap images are about 40% smaller with x86_64_32, this is > not always the case; some heap images ended up being even larger in > this experiment. Could there be a problem with the sharing pass on > x86_64_32? There was indeed something odd with sharing: David Matthews has changed that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46). > Hardware: > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD > > Common build flags: > ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2" > > Configurations: > polyml 5.7.1x86_64ML_OPTIONS="--maxheap 24G -H 500 --gcthreads > 6" > polyml-a444f281ccec x86_64ML_OPTIONS="--maxheap 24G -H 500 --gcthreads > 6" For this hardware I recommend threads=6. Moreover note that --gcthreads is automatically provided, if ML_OPTIONS does not say anything else. > 623083120 IsaFoR_2 (1.00) > 623291272 IsaFoR_2 (1.00) > 367497971 IsaFoR_2 (0.59) > 884213127 IsaFoR_2 (1.42) ? I have briefly tried IsaFoR_2 and now get 624867156 (1.00), which is better but still slightly odd. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)
On 23/01/2019 23:44, Makarius wrote: > Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec > (active by default). > > It performs slightly better than the previous test version -- I have > also removed old workarounds for integer arithmetic in > Isabelle/4591221824f6. One more performance result in this respect: Isabelle/4591221824f6 + AFP/2eacf2ed7d5d x86_64_32-linux --minheap 1500 threads=8 Finished Flyspeck-Tame (3:37:32 elapsed time, 5:32:38 cpu time, factor 1.53) This is a about two times better than what we were used to. It is a combination of high-end software (current Poly/ML) with high-end hardware (Intel Xeon Gold 6148 CPU @ 2.40GHz, 20 CPU cores, 64 GB memory, SSD). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)
Isabelle/20bc1d26c932 now provides an updated polyml-test-a444f281ccec (active by default). It performs slightly better than the previous test version -- I have also removed old workarounds for integer arithmetic in Isabelle/4591221824f6. It is important to check that obsolete entries in $ISASELLE_HOME_USER/etc/settings are cleaned up, such that this greatest and latest version gets used. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 23/01/2019 12:05, David Matthews wrote: > > I've had a look at this under Windows and the problem seems to be with > calls to IntInf.divMod from generated code, not from IntInf.pow. The > underlying RTS call used by IntInf.quotRem has changed in the 32-in-64 > version. It previously returned the pair of values by passing in a > stack location and having the RTS update this. That isn't possible in > the 32-in-64 version so now it allocates a pair on the heap. For > simplicity this is now used for the native code versions as well. From > what I can tell nearly all the threads are waiting for mutexes and I > suspect that the extra heap allocation in IntInf.quotRem is causing some > of the problem. Waiting for a contended mutex can cost a significant > amount of processor time both in busy-waiting and in kernel calls. > > I'm not sure what to suggest except not to use concurrency here. There > doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem. In the meantime David has produced Poly/ML a444f281ccec and I can confirm that it works very well: Isabelle/2444c8b85aac AFP/2eacf2ed7d5d x86_64_32-linux --minheap 1500 threads=8 Finished HOL-ODE-Numerics (0:17:18 elapsed time, 0:45:28 cpu time, factor 2.63) Finished Lorenz_C0 (0:12:06 elapsed time, 1:29:19 cpu time, factor 7.37) x86_64-linux --minheap 1500 threads=8 Finished HOL-ODE-Numerics (0:19:19 elapsed time, 0:49:46 cpu time, factor 2.58) Finished Lorenz_C0 (0:06:54 elapsed time, 0:50:34 cpu time, factor 7.33) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 23/01/2019 14:14, Bertram Felgenhauer wrote: > Makarius wrote: >> On 22/01/2019 12:31, Bertram Felgenhauer wrote: >>> Makarius wrote: >>>> So this is the right time for further testing of applications: >>>> Isabelle2018 should work as well, but I have not done any testing beyond >>>> "isabelle build -g main" -- Isabelle development only moves forward in >>>> one direction on a single branch. >>> >>> I have tried this with Isabelle2018 and IsaFoR; I've encountered no >>> problems and there's a nice speedup (estimated 1.25 times faster). >>> Heap images are 40% smaller, which is a welcome change as well. >> >> Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)? > > This is compared to x86_64. Sorry, I should have mentioned this, > but to my mind it was implied because IsaFoR is notorious for running > out of memory with the x86 version of PolyML. OK, this is the kind of applications that x86_64_32 has been made for: less memory requirements (< 16 GB) and much faster within it. >> I am asking this, because I have noted a speedup of building heap >> images: x86_64_32 compared to x86, and was wondering about the reasons >> for it. (For x86_64 everything is just more bulky, of course, including >> heaps.) > > As far as I can see, one difference between x86 and x86_64_32 is that > PolyML keeps heap objects aligned to 8 byte boundaries for the latter. > This may impact performance. I misinterpreted my earlier measurements: the test version is actually a bit slower in dumping heap images, but x86 is worse than x86_64_32 in this respect. Something to be investigated further ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 22/01/2019 23:08, Fabian Immler wrote:
> On 1/22/2019 4:00 PM, Fabian Immler wrote:
>> On 1/22/2019 2:28 PM, Makarius wrote:
>>> On 22/01/2019 20:05, Fabian Immler wrote:
>>>> These numbers look quite extreme:
>>>> The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
>>>> it seems to be the case with polyml-test-0a6ebca445fc).
>>>>
>>>> The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:
>>>>
>>>> ML_PLATFORM="x86-linux"
>>>> ML_OPTIONS="--minheap 2000 --maxheap 4000"
>>>> Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time,
>>>> factor 2.66)
>>>> Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time,
>>>> factor 1.46) > (I am testing HOL-ODE-ARCH-COMP with
>> polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take
>> some time...)
> HOL-ODE-ARCH-COMP looked fine (2-3 times slower). But I realized that
> this was the case with your computations, too. Unlike Lorenz_C0:
>
>> x86_64_32-linux -minheap 1500
>> Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44)
>> x86_64-linux --minheap 3000
>> Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52)
> Lorenz_C0 had the most significant slowdown, it has the biggest number
> of parallel computations, so I thought this might be related.
>
> And indeed, if you try the theory at the end:
> Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32
> whereas the sequential evaluation is only 2 times slower.
>
> All of this reminds me of the discussion we had in November 2017:
> https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2017-November/thread.html#7643
Back in Nov-2017, I made the following workaround that is still active:
http://isabelle.in.tum.de/repos/isabelle/rev/5da20135f560
Looking at the profiles of the included Float_Test.thy I now see a lot
of IntInf.divMod, but it is qualitatively similar to former IntInf.pow.
Maybe David can revisit both of these operations, so that we can get
rid of the workarounds.
Note that I have produced the profiles as follows:
isabelle build -o profiling=time ...
with a suitable test session that includes the above test theory, e.g.
see the included ROOT.
Then with "isabelle profiling_report" on the resulting log files, e.g.
isabelle profiling_report
~/.isabelle/heaps/polyml-5.7.1_x86-linux/log/Float_Test.gz
Makarius
theory Float_Test
imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin
definition "logistic p r x =
normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down
p 1 (-x)))"
primrec iter where
"iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"
definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1))
(nat_of_integer i)"
ML \val logistic_chaos = @{code logistic_chaos}\
ML \Par_List.map logistic_chaos (replicate 10 10)\
\ \x86_64_32: 24s
x86_64: 2s\
(*
ML \map logistic_chaos (replicate 10 10)\
\ \x86_64_32: 16s
x86_64: 8s\
*)
endsession Float_Test = "HOL-Library" +
theories
Float_Test
Float_Test:
1 eq-xsymb
1 Term_Ord.typ_ord
1 Raw_Simplifier.extract_rews
1 Output_Primitives.ignore_outputs
1 Code_Symbol.symbol_ord
1 Proofterm.thm_ord
1 Multithreading.sync_wait
1 Graph().merge_trans_acyclic
1 Scan.many
1 Basics.fold_map
1 Basics.fold
1 Pretty.string
1 Type_Infer_Context.prepare_term
1 eq-xprod
1 Term.add_tvarsT
1 Print_Mode.print_mode_value
1 X86ICodeToX86Code().icodeToX86Code
1 ProofRewriteRules.rew
1 String.fields
1 List.foldr
1 Library.insert
1 Type_Infer_Context.unify
1 Term.fold_aterms
1 Term.fastype_of1
1 Raw_Simplifier.bottomc
1 Term_Ord.fast_indexname_ord
1 Term_Subst.map_aterms_same
1 Type_Infer.add_parms
1 Axclass.unoverload
1 CODETREE_REMOVE_REDUNDANT().cleanProc
1 X86ICodeIdentifyReferences().getInstructionState
1 IntSet.minusLists
1 Term_Subst.map_types_same
1 Symbol.explode
1 Graph().add_edge
1 TYPE_TREE().eventual
1 Raw_Simplifier.rewrite_rule_extra_vars
1 Path.check_elem
1 Lazy.force_result
1 Raw_Simplifier.insert_rrule
1 Term.map_types
1 Induct().concl_var
Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith
On 22/01/2019 22:02, Florian Haftmann wrote:
>
> Then I have no clue how to include the installed zarith properly.
> https://opam.ocaml.org/doc/FAQ.html mentions subcommands »exec« and
> »env« for opam, which the installed version available through »isabelle
> ocaml_opam« does not provide.
That documentation is for Opam 2.0, but we are still on 1.2.2 because
that is the latest version I've found for Windows (based on MinGW); the
same 1.2.2 is part of Cygwin.
I can update Isabelle/Opam when there is a proper Windows version for
2.0 -- maybe it has already arrived in the meantime, somewhere in some
dark corner.
Apart from that, I've recently seen Coq experts worry about the
status-quo of Opam: it is not as well-developed as Stack for Haskell,
and Coq already critically depends on it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 22/01/2019 20:05, Fabian Immler wrote: > These numbers look quite extreme: > The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as > it seems to be the case with polyml-test-0a6ebca445fc). > > The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0: > > ML_PLATFORM="x86-linux" > ML_OPTIONS="--minheap 2000 --maxheap 4000" > Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time, > factor 2.66) > Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time, > factor 1.46) Can you point to some smaller parts of these sessions, where the effect is visible? We can then use profiling to get an idea what actually happens in x86_64_32. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" > > It requires the usual "isabelle components -a" incantation afterwards. polyml-test-0a6ebca445fc is the default in 81ca77cb7c8c, it means the scope of further testing has widened. Almost everything has become faster by default, but an exception are heavy-duty int computations that rely on a certain word size, notably the HOL-ODE family of sessions. AFP/a04825886e71 marks various sessions explicitly as "large", which means that they prefer x86_64. Here are concrete numbers: x86_64_32-linux -minheap 1500 Finished Pure (0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00) Finished HOL (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45) Finished HOL-Analysis (0:03:48 elapsed time, 0:21:27 cpu time, factor 5.64) Finished Ordinary_Differential_Equations (0:01:14 elapsed time, 0:05:31 cpu time, factor 4.43) Finished Differential_Dynamic_Logic (0:01:29 elapsed time, 0:05:03 cpu time, factor 3.39) Finished HOL-ODE-Numerics (0:17:51 elapsed time, 0:46:30 cpu time, factor 2.60) Finished Lorenz_Approximation (0:04:02 elapsed time, 0:07:46 cpu time, factor 1.92) Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10) Finished HOL-ODE-ARCH-COMP (0:12:56 elapsed time, 0:28:35 cpu time, factor 2.21) Finished HOL-ODE-Examples (0:37:13 elapsed time, 2:51:00 cpu time, factor 4.59) Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44) x86_64-linux --minheap 3000 Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 1.00) Finished HOL (0:02:44 elapsed time, 0:09:28 cpu time, factor 3.47) Finished HOL-Analysis (0:04:05 elapsed time, 0:22:47 cpu time, factor 5.58) Finished Ordinary_Differential_Equations (0:01:19 elapsed time, 0:05:49 cpu time, factor 4.40) Finished Differential_Dynamic_Logic (0:01:33 elapsed time, 0:05:22 cpu time, factor 3.44) Finished HOL-ODE-Numerics (0:18:59 elapsed time, 0:49:00 cpu time, factor 2.58) Finished Lorenz_Approximation (0:04:01 elapsed time, 0:07:39 cpu time, factor 1.90) Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.20) Finished HOL-ODE-ARCH-COMP (0:04:06 elapsed time, 0:08:37 cpu time, factor 2.10) Finished HOL-ODE-Examples (0:05:18 elapsed time, 0:17:04 cpu time, factor 3.22) Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 22/01/2019 12:31, Bertram Felgenhauer wrote: > Makarius wrote: >> So this is the right time for further testing of applications: >> Isabelle2018 should work as well, but I have not done any testing beyond >> "isabelle build -g main" -- Isabelle development only moves forward in >> one direction on a single branch. > > I have tried this with Isabelle2018 and IsaFoR; I've encountered no > problems and there's a nice speedup (estimated 1.25 times faster). > Heap images are 40% smaller, which is a welcome change as well. Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)? I am asking this, because I have noted a speedup of building heap images: x86_64_32 compared to x86, and was wondering about the reasons for it. (For x86_64 everything is just more bulky, of course, including heaps.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
On 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" > > It requires the usual "isabelle components -a" incantation afterwards. Here are some performance measurements on the best hardware that I have presently access to (not at TUM): Intel Xeon Gold 6148 CPU @ 2.40GHz 20 CPU cores * 2 hyperthreads * 2 nodes 64 GB memory SSD Isabelle/2633e166136a + AFP/ba82c831e5c2 isabelle build -N -j2 -o threads=8 x86-linux --minheap 1500 --maxheap 3500 Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37) Finished HOL (0:02:36 elapsed time, 0:08:46 cpu time, factor 3.37) Finished HOL-Analysis (0:03:49 elapsed time, 0:21:11 cpu time, factor 5.55) Finished HOL-Analysis (0:03:50 elapsed time, 0:21:19 cpu time, factor 5.55) Finished HOL-Data_Structures (0:01:39 elapsed time, 0:11:30 cpu time, factor 6.91) Finished HOL-Data_Structures (0:01:43 elapsed time, 0:11:52 cpu time, factor 6.87) Finished HOL-Nominal (0:00:28 elapsed time, 0:01:07 cpu time, factor 2.34) Finished HOL-Nominal (0:00:29 elapsed time, 0:01:08 cpu time, factor 2.33) Finished HOL-Nominal-Examples (0:02:57 elapsed time, 0:14:11 cpu time, factor 4.80) Finished HOL-Nominal-Examples (0:03:09 elapsed time, 0:14:55 cpu time, factor 4.73) Finished HOL-Proofs (0:09:52 elapsed time, 0:23:45 cpu time, factor 2.41) Finished HOL-Proofs (0:09:52 elapsed time, 0:24:04 cpu time, factor 2.44) x86_64_32-linux --minheap 1500 --maxheap 3500 Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.49) Finished HOL (0:02:32 elapsed time, 0:08:50 cpu time, factor 3.48) Finished HOL-Analysis (0:03:41 elapsed time, 0:20:56 cpu time, factor 5.67) Finished HOL-Analysis (0:03:39 elapsed time, 0:20:50 cpu time, factor 5.70) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:33 cpu time, factor 7.16) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:35 cpu time, factor 7.20) Finished HOL-Nominal (0:00:12 elapsed time, 0:00:24 cpu time, factor 2.07) Finished HOL-Nominal (0:00:11 elapsed time, 0:00:24 cpu time, factor 2.06) Finished HOL-Nominal-Examples (0:02:53 elapsed time, 0:13:54 cpu time, factor 4.82) Finished HOL-Nominal-Examples (0:02:51 elapsed time, 0:13:51 cpu time, factor 4.83) Finished HOL-Proofs (0:09:55 elapsed time, 0:23:48 cpu time, factor 2.40) Finished HOL-Proofs (0:09:48 elapsed time, 0:23:35 cpu time, factor 2.40) x86_64_32-linux --minheap 3000 --maxheap 7000 Finished HOL (0:02:32 elapsed time, 0:08:53 cpu time, factor 3.50) Finished HOL (0:02:32 elapsed time, 0:08:51 cpu time, factor 3.49) Finished HOL-Analysis (0:03:26 elapsed time, 0:20:06 cpu time, factor 5.84) Finished HOL-Analysis (0:03:45 elapsed time, 0:21:20 cpu time, factor 5.67) Finished HOL-Data_Structures (0:01:35 elapsed time, 0:11:32 cpu time, factor 7.26) Finished HOL-Data_Structures (0:01:36 elapsed time, 0:11:36 cpu time, factor 7.20) Finished HOL-Nominal (0:00:12 elapsed time, 0:00:25 cpu time, factor 2.08) Finished HOL-Nominal (0:00:11 elapsed time, 0:00:25 cpu time, factor 2.10) Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time, factor 4.88) Finished HOL-Nominal-Examples (0:02:45 elapsed time, 0:13:26 cpu time, factor 4.87) Finished HOL-Proofs (0:08:10 elapsed time, 0:19:17 cpu time, factor 2.36) Finished HOL-Proofs (0:08:23 elapsed time, 0:19:13 cpu time, factor 2.29) x86_64-linux --minheap 1500 --maxheap 7000 Finished HOL (0:02:48 elapsed time, 0:09:46 cpu time, factor 3.48) Finished HOL (0:02:46 elapsed time, 0:09:34 cpu time, factor 3.45) Finished HOL-Analysis (0:04:01 elapsed time, 0:22:39 cpu time, factor 5.64) Finished HOL-Analysis (0:04:00 elapsed time, 0:22:27 cpu time, factor 5.60) Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:49 cpu time, factor 6.47) Finished HOL-Data_Structures (0:01:58 elapsed time, 0:12:42 cpu time, factor 6.46) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.05) Finished HOL-Nominal (0:00:13 elapsed time, 0:00:27 cpu time, factor 2.04) Finished HOL-Nominal-Examples (0:03:03 elapsed time, 0:14:39 cpu time, factor 4.80) Finished HOL-Nominal-Examples (0:02:58 elapsed time, 0:14:29 cpu time, factor 4.88) Finished HOL-Proofs (0:10:16 elapsed time, 0:25:24 cpu time, factor 2.47) Finished HOL-Proofs (0:10:21 elapsed time, 0:25:35 cpu time, factor 2.47) x86_64-linux --minheap 3000 --maxheap 14000 Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.46) Finished HOL (0:02:44 elapsed time, 0:09:31 cpu time, factor 3.47) Finished HOL-Analysis (0:04:06 elapsed time, 0:22:40 cpu time, factor 5.51) Finished HOL-Analysis (0:04:06 elapsed time, 0:22:54 cpu time, factor 5.57) Finished HOL-Data_Structures (0:01:44 elapsed time, 0:12:28 cpu time, factor 7.14) Fini
[isabelle-dev] Poly/ML x86_64_32 available for testing
Thanks to great work by David Matthews, there is now an Isabelle component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc" It requires the usual "isabelle components -a" incantation afterwards. This supports 3 platform variants: x86 x86_64 x86_64_32 x86 is still there for comparison, but will disappear soon. x86_64 is the full 64-bit model as before, and subject to the system option "ML_system_64 = true". x86_64_32 is the default. It is a synthesis of the x86_64 architecture (more memory, more registers etc.) with a 32-bit value model for ML. Thus we get approx. 5 times more memory as in x86, without the penalty of full 64-bit values. Moreover, we have a proper "64-bit application" according to Apple (and Linux distributions): it is getting increasingly hard to run old x86 executables, and soon it might be hardly possible at all. In other words, Poly/ML is now getting ready for many more years to come. The above component already works smoothly for all of Isabelle + AFP, only with spurious drop-outs that can happen rarely. x86_64_32 is already more stable than x86, which often suffers from out-of-memory situations. So this is the right time for further testing of applications: Isabelle2018 should work as well, but I have not done any testing beyond "isabelle build -g main" -- Isabelle development only moves forward in one direction on a single branch. For really big applications, it might occasionally help to use something like "--maxheap 8g" in ML_OPTIONS: the implicit maximum is 16g, which is sometimes too much for many parallel jobs on mid-range hardware. There are additional memory requirements outside the ML heap, for program code and stacks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
On 18/01/2019 21:55, Tobias Nipkow wrote: > Hey, I wanted to join the party! But all bugs have been fixed now and > Makarius will notify you of the correct changeset. Yes, see Isabelle/b18353d3fe1a. Despite the carnival season, I am presently working with David Matthews to make the canononical "isabelle build -a" invocations faster and less painful than ever -- the normal routine of many years. There are reasons why Isabelle + AFP has become so great in the past 10 years, and I am serious about continuing this. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
On 17/01/2019 22:54, Fabian Immler wrote: > > Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong > during the merges, so I could easily redo Angeliki's tagging (689997a8). > > We should be back to normal (regarding isabelle build -a). That was Isabelle/94284d4dab98, but Tobias has just pushed a bad merge again: Isabelle/aeceb14f387a. I can only quote README_REPOSITORY once more: Testing of changes (before push) The integrity of the standard pull/push area of Isabelle needs the be preserved at all time. This means that a complete test with default configuration needs to be finished successfully before push. If the preparation of the push involves a pull/merge phase, its result needs to covered by the test as well. Such testing of local changes plus the resulting merge is not optional, but mandatory. There is a natural routine of "hg commit" vs. "isabelle build -a" to make it all work well without any effort. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
On 18/01/2019 11:42, Lars Hupel wrote: >> The problem behind this: Angeliki got administrative push-access to the >> Isabelle repository, without anybody at Cambridge showing her how to use it. > > Before we start blaming individual people, this is not a person problem, > but a tooling problem. Industry has figured out this problem years ago. > One doesn't simply allow pushes to master (or "default" in Mercurial). > CakeML has adopted this too. I did not blame anybody, merely pointed out the actual problem. README_REPOSITORY gives a lot of explanations, including our important model of having just one branch, i.e. no branches at all. With further branches, the situation would become much worse, like the average project on github. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
On 17/01/2019 21:54, Makarius wrote: > > The problem behind this: Angeliki got administrative push-access to the > Isabelle repository, without anybody at Cambridge showing her how to use it. > > There is of course README_REPOSITORY, but the text is long. Here is the > ultra-short version: > > After every local commit, use "hg view" (or equivalent) to ensure that > the change is really what you want to make eternal when pushed to public. Here is another (minor) error by Angeliki: 6b8d78186947 is actually a merge (a clean one according to "hg view"), but the log message makes it appear like a regular change. (README_REPOSITORY explains proper treatment of merge nodes.) I've seen that incident already on Monday -- still with a high temperature, and not in proper shape to look more closely or write private mails etc. Instead, I was watching silly things like https://www.youtube.com/watch?v=FOJtmDYcFMg -- not totally unrelated to this thread. Maybe Larry can show Angeliki how to operate the "hg" chainsaw adequately. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mercurial accident
On 17/01/2019 21:42, Lars Hupel wrote: >> Strip the accidental changes from the repository? > > Never strip public changesets. Indeed. "Fixing" a desaster by non-monotonic operations is a desaster squared. > >> Back out the changes? > > You can't really back out merges, as far as I know. > >> Or do a no-op merge from a successor of the last working version? > > This is also not possible, I think. > > Do this instead: > > $ hg revert -a -r 56acd449da41 > $ hg commit -m "revert to 56acd449da41" This looks fine and obvious. The problem behind this: Angeliki got administrative push-access to the Isabelle repository, without anybody at Cambridge showing her how to use it. There is of course README_REPOSITORY, but the text is long. Here is the ultra-short version: After every local commit, use "hg view" (or equivalent) to ensure that the change is really what you want to make eternal when pushed to public. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Website https://isabelle.in.tum.de is down
On 14/01/2019 18:47, Makarius wrote: > The website https://isabelle.in.tum.de appears to be down, this also > includes the Mercurial repository view at > https://isabelle.sketis.net/repos/isabelle > > Access via SSH works fine, thus the following clone is up-to-date within > an interval of 10min: https://isabelle.sketis.net/repos/isabelle That is the same repository URL twice -- I should not write mails with a temperature. The following notable HTTPS services are down: https://isabelle.in.tum.de https://isabelle.in.tum.de/repos/isabelle https://isabelle.in.tum.de/devel Here are mirrors that work: https://www.cl.cam.ac.uk/research/hvg/Isabelle https://isabelle.sketis.net/repos/isabelle https://isabelle.sketis.net/devel Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Website https://isabelle.in.tum.de is down
The website https://isabelle.in.tum.de appears to be down, this also includes the Mercurial repository view at https://isabelle.sketis.net/repos/isabelle Access via SSH works fine, thus the following clone is up-to-date within an interval of 10min: https://isabelle.sketis.net/repos/isabelle Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 11/01/2019 11:51, Makarius wrote: > On 10/01/2019 16:38, Makarius wrote: >> On 10/01/2019 16:28, Florian Haftmann wrote: >>> Code generation: command 'export_code' without file keyword exports >>> code as regular theory export, which can be materialized using tool >>> 'isabelle export'; to get generated code dumped into output, use >>> 'file ""'. Minor INCOMPATIBILITY. >>> >>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc >>> generated code in AFP-entries. >> >> Great, I will try this out soon. > > I have started looking and thinking about it again. I have reworked this a bit in Isabelle/e61b0b819d28: Isabelle/jEdit is able to browse theory exports via the virtual file-system "isabelle-export:" and the 'export_code' command emits some information message about it. There are still a few open questions: * Are there remaining uses of 'file' with empty name? Is the virtual file-system browser sufficiently convenient to inspect results interactively? * How to specify proper (unique) export names: PIDE still lacks a check for uniqueness of export names, but overwriting existing exports is considered illegal. The 'file' allowed to produce separate names in the past, but it has a different meaning now (and is a candidate for deletion). Maybe 'export_code' should be renovated replaced by reformed commands like this: * "code_export PREFIX = CONSTS in LANGUAGE" where the PREFIX is optional and the default something like "generated" or "code". This could be a "thy_decl" command that updates the theory context by generated files that are accessible in Isabelle/ML, in addition to the export; it would also include a check for duplicate names. * "code_checking CONSTS in LANGUAGE" -- observing that "export_code ... checking" is actually a different command. It would be a "diag" command as before (this is relevant for parallelism). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 10/01/2019 16:38, Makarius wrote:
> On 10/01/2019 16:28, Florian Haftmann wrote:
>> Code generation: command 'export_code' without file keyword exports
>> code as regular theory export, which can be materialized using tool
>> 'isabelle export'; to get generated code dumped into output, use
>> 'file ""'. Minor INCOMPATIBILITY.
>>
>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
>> generated code in AFP-entries.
>
> Great, I will try this out soon.
I have started looking and thinking about it again.
First note that Export.export_raw is only required for very big exports
that have their own compression somehow built in. You can always use
Export.export in regular applications: the compression status is stored
in the database, and the exported result is uncompressed.
> I've had some discussions with users of Haskell code generation, e.g.
> AFP/HLDE.
>
> My conclusions so far:
>
> * primary (default) output should be via the new Generated_Files
> module in Isabelle/ML; thus applications can refer to file content via a
> theory context, e.g. to write it to the file-system via
> Generated_Files.write_files.
>
> * secondary output works via the Export interface to Isabelle/Scala;
> e.g. I could easily add Generated_Files.export_files for that and
> export_code would merely use Generated_Files.add_files (no export yet).
I have added Generated_Files.export_files in Isabelle/a2fbfdc5e62d: the
generated sources from Isabelle/Haskell serve as an example.
How to proceed from here is still unclear. I will look more closely at
the applications of 'export_code' in AFP. The question is if we can get
rid of all options for experimentation ('file') and have the Prover IDE
and system environment take care of it.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: generated code as proper theory export
On 10/01/2019 16:28, Florian Haftmann wrote: > Code generation: command 'export_code' without file keyword exports > code as regular theory export, which can be materialized using tool > 'isabelle export'; to get generated code dumped into output, use > 'file ""'. Minor INCOMPATIBILITY. > > This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc > generated code in AFP-entries. Great, I will try this out soon. On Mon..Wed this week I visited the Innsbruck Isabelle site (the city of Innsbruck is very professional in managing a lot of snow without hindering public life :-) I've had some discussions with users of Haskell code generation, e.g. AFP/HLDE. My conclusions so far: * primary (default) output should be via the new Generated_Files module in Isabelle/ML; thus applications can refer to file content via a theory context, e.g. to write it to the file-system via Generated_Files.write_files. * secondary output works via the Export interface to Isabelle/Scala; e.g. I could easily add Generated_Files.export_files for that and export_code would merely use Generated_Files.add_files (no export yet). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: isabelle update
*** System ***
* The command-line tool "isabelle update" uses Isabelle/PIDE in
batch-mode to update theory sources based on semantic markup produced in
Isabelle/ML. Actual updates depend on system options that may be enabled
via "-u OPT" (for "update_OPT"), see also $ISABELLE_HOME/etc/options
section "Theory update". Theory sessions are specified as in "isabelle
dump".
This refers to Isabelle/1d2d4ae9ab81 and there is some documentation in
the "system" manual as usual. The "isabelle update" tool is a corollary
of the "Headless PIDE" session; it opens new possibilities for
systematic maintenance of formal sources at a large scale. In the next
round I will provide options to replace old-style ASCII syntax, e.g. %
== ==> -->.
An example is Isabelle/a96320074298, which is the result of applying
"isabelle update -u path_cartouches" for all sessions.
So far I have refrained from too much updating, because I am not sure
how far we are in the process of mental adaption, to see cartouches
almost everywhere. In particular "isabelle update -u
inner_syntax_cartouches" will be quite significant:
* Different visual appearance of Isabelle sources: potentially odd for
long-term users, but less odd for newcomers (i.e. no longer questions
like "What is the meaning of double-quotes around the logical language?"
at first-time exposure).
* It potentially affects corner cases for implicit or explicit
double-quotes in document preparation (cf. options thy_output_quotes /
thy_output_source or @{term [quotes] "..."} / @{term [source] "..."}).
* When inner syntax double-quotes are discontinued eventually, the
inner syntax of the HOL library may use double quotes for char/string
literals, instead of slightly odd double single-quotes.
Here is a reminder of the general approach and trend of recent years:
* embedded languages normally use cartouches, while double quotes are
old-style / legacy;
* names normally use plain identifiers, but double quotes are
available to escape conflicts with keywords.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Update of Haskell Stack
Here are some notable changes concerning the Haskell Stack, which is a build tool with a package repository behind it: changeset: 69526:5574d504cf36 tag: tip user:wenzelm date:Fri Dec 28 19:01:35 2018 +0100 files: etc/settings description: more conservative update of Haskell stack (amending 04e54f57a869): 13.0 still lacks notable packages like "Agda" or "darcs"; changeset: 69512:04e54f57a869 parent: 69506:7d59af98af29 user:Lars Hupel date:Thu Dec 27 17:36:19 2018 +0100 files: etc/settings src/Pure/General/path.ML description: update LTS Haskell version I am myself still in the process of learning how the Stack community and release process works. Spending 5 min with the announcement of lts-13.0 from Isabelle/04e54f57a869 leaves the impression that a new major release is merely the factual start for package maintainers to become serious about updating and publishing their stuff. Haskell Stack LTS versions should appear every 3-6 months -- according to the official statement https://github.com/commercialhaskell/lts-haskell#readme So it looks like it is better to stay one major release version behind the frontier of ongoing LTS development. Moreover, I have so far refrained from updating minor versions without particular reasons: it always causes a lot of network traffic and disk usage increase for local .stack directories. Here is also a concrete project that refers to Isabelle/Haskell from isabelle-dev and is in sync with its Stack version: https://github.com/Naproche/Naproche-SAD/commit/2af938e09a61c14f57af40679bb340a92b521331 This proves the use and usability of the emerging Isabelle/Haskell infrastructure. In the longer term it might help more users out there to develop Haskell-based projects for Isabelle; or just use other ITP systems like Agda -- when OPAM gets into better shape we could also apply this principle to Coq. Overall, the general approach of the Isabelle distribution is to deliver canonical versions of add-on tools that just work without manual tinkering. Thus "latest" things require more than one close look before adopting them. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?
On 27/12/2018 17:45, Traytel Dmitriy wrote: > Hi Larry, > > the HOL-Cardinals library might be just right for the purpose: > > theory Scratch > imports "HOL-Cardinals.Cardinals" > begin > > lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)" > by (rule card_of_ordLeq[symmetric]) > > lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)" > by (rule card_of_ordIso[symmetric]) > > lemma > assumes "|A| ≤o |B|" "|B| ≤o |A|" > shows "|A| =o |B|" > by (simp only: assms ordIso_iff_ordLeq) > > end > > The canonical entry point for the library is the above > HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in > Main, because the (co)datatype package is based on them. The syntax is hidden > in main—one gets it by importing HOL-Library.Cardinal_Notations (which > HOL-Cardinals.Cardinals does transitively). It would be great to see this all consolidated and somehow unified, i.e. some standard notation in Main as proposed by Larry (potentially as bundles as proposed by Florian), and avoidance of too much no_syntax remove non-standard notation from Main. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 21:56, Makarius wrote: > On 30/11/2018 19:45, Thomas Sewell wrote: > > I am also unsure why "archive formats" got on this thread. The heap is a > binary build artifact, with its own internal structure. Its precise > content is somewhat non-deterministic, even when everything runs in > sequential mode (which is very slow and hardly ever done). > > It works due to some special trickery for the main Isabelle sessions > (and in Isabelle2018 also for AFP) via Path.smart_implode, to fold > physical file locations back into symbolic form: $ISABELLE_HOME/src/... > or $AFP/... Another side-remark: Poly/ML does store an absolute path for the imported heap hierarchy, but Isabelle/ML ignores that: it uses freshly resolved file names with PolyML.SaveState.loadHierarchy. Only the logical session name and the SHA1 key is taken into account for dependency management. I've confirmed that with my experiment: using the "strings" tool on the heap file yields precisely one file name in my own home directory (where everything was built): it is the (unused) physical heap file name (before moving the whole installation). [All of this with official Isabelle2018 -- and all this discussion properly belongs to the isabelle-users mailing list. There is no mailing list for "packaging of Isabelle for Linux distributions".] Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 19:45, Thomas Sewell wrote: > I'd just like to confirm that other users have seen this issue. > Colleagues of mine > > have tried to pre-build heaps on a build server and share them with other > users. It could have saved CPU-hours, and in some cases, hours of humans > waiting around, but it never worked. > > My understanding is that the "hash the world" mechanism for capturing > the state of the dependencies sometimes captures the absolute names of > files. > This breaks down in the obvious way if, for instance, we can't assume > that all > the target users have the same username. None of this has anything to do > with the archive format. I am also unsure why "archive formats" got on this thread. The heap is a binary build artifact, with its own internal structure. Its precise content is somewhat non-deterministic, even when everything runs in sequential mode (which is very slow and hardly ever done). The starting point was about the HOL image, where movable images should work under normal circumstances (I've just tried that a few hours ago). But having a build-server for HOL is usually pointless, because it merely requires 2-5min to build on the spot (and much slower hardware is unusable for Isabelle applications). It works due to some special trickery for the main Isabelle sessions (and in Isabelle2018 also for AFP) via Path.smart_implode, to fold physical file locations back into symbolic form: $ISABELLE_HOME/src/... or $AFP/... I can't say for sure about images outside Isabelle + AFP, but I've occasionally heard about users managing even that (e.g. IsaFoR in Innsbruck). Maybe this was based on a homogeneous file-system layout. Of course, there can be many other ways in user-space to refer persistently to physical file locations, or to build other non-portable information into the heap. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 18:56, Jonathon Fernyhough wrote: >> >>> However, a Debian packaging file is the correct approach for local >>> deployment to multiple Debian/Ubuntu machines. >> >> It is one approach, but typically causes problems. > > Given the size of the Debian repositories and the range of software they > make available I'm not really sure this is true. Hopefully this is not another attempt at an official Debian package of Isabelle. Many years ago, some people tried it, but it always caused more problems than it solved. And today the system is more complex and more easily destroyed by packaging it. These days I see big and complex products doing it our way: providing a fully integrated distribution for end-users that by-passes OS package managers. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 16:30, Jonathon Fernyhough wrote: > On 30/11/2018 14:55, Makarius wrote: >> On 30/11/2018 14:15, Jonathon Fernyhough wrote: >>> >>> I'm currently packaging Isabelle2018 (in deb format) for deployment to >>> several machines. These packages should contain some default heaps so >>> users can get on with what they're doing and avoid duplicating hundreds >>> of megabytes of data across user profiles. >>> >>> I'm trying to automate the heap build process using the debian/rules >>> file in the "standard" way but the generated heaps are seen as >>> out-of-date when the user runs the Isabelle GUI, which then tries to >>> regenerate the heaps (and fails because the system directory isn't >>> writable). >> >> There is no point do "debianize" Isabelle: it is a plain user-space >> application program, not a system component. >> > > You're correct that there's no need to do this if you're a single user > running Isabelle on a single machine. Isabelle dates back from a time of multi-user / multi-platform installations, although that is rarely used these days. This scheme still works. It is even more general than Debianization. > However, a Debian packaging file is the correct approach for local > deployment to multiple Debian/Ubuntu machines. It is one approach, but typically causes problems. >> You should be able to achive the above without deb packaging like this: >> >> * unpack the Isabelle tar.gz >> * run "Isabelle/bin/isabelle build -s -b HOL" (or any other images >> that users might need) >> * copy the result to the target (e.g. via "cp -a" or as a tar.gz) >> >> Here "Isabelle" refers to any Isabelle distribution from recent years: >> it is normal that Isabelle users have more than one of it active. > > I suppose that would be a workaround - build the heaps as part of > packaging process but archive them, then extract them during installation. Isn't this the normal way of packaging build artifacts? >> Also note that "isabelle build" uses SHA1 hash keys on the sources, not >> datestamps. > > This raises a different question of why the **sources** SHA1 hashes are > different between the packaging chroot (pbuild/sbuild) and the local system. > > What is being hashed? A full path or just the filename? Just the content of everything that is required: sources, other heaps etc. There is one side-condition: the file-system needs to be reasonably sane to allow folding file names back to the symbolic form of ~~/src/HOL/ROOT etc. -- my guess it that the funny Debian build environment somehow destroys that. (BTW: nothing of this is relevant to the isabelle-dev mailing list.) Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts
On 24/11/2018 19:51, Makarius wrote: > > *** Isabelle/jEdit Prover IDE *** > > * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle > DejaVu" collection by default, which provides uniform rendering quality > with the usual Isabelle symbols. For Java/Swing GUI elements this > requires the Metal look-and-feel: it is the default on Linux, but not > macOS nor Windows. Line spacing no longer needs to be adjusted: > properties for the old IsabelleText font had "Global Options / Text Area > / Extra vertical line spacing (in pixels): -2", now it defaults to 0. I have reworked this further in various changesets leading up to Isabelle/429426640596. In particular, the Isabelle fonts are now forced on all Java/Swing look-and-feels, by modifying some UIManager font properties. This appears to work reasonably well on Linux GTK+, Windows, Mac OS X, but we need to keep an eye on it for fine points and drop-outs. (For Metal look-and-feel and already worked uniformly before.) The idea is that GUI elements use "Isabelle DejaVu Sans" (not "Mono") wherever feasible. Thus all mathematical symbols and special icons should be always correctly displayed (e.g. in Hypersearch tree view). The regular search dialog now also uses this font: before it was the main text area font (usually the "Mono" version). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH
On 30/11/2018 14:15, Jonathon Fernyhough wrote: > > I'm currently packaging Isabelle2018 (in deb format) for deployment to > several machines. These packages should contain some default heaps so > users can get on with what they're doing and avoid duplicating hundreds > of megabytes of data across user profiles. > > I'm trying to automate the heap build process using the debian/rules > file in the "standard" way but the generated heaps are seen as > out-of-date when the user runs the Isabelle GUI, which then tries to > regenerate the heaps (and fails because the system directory isn't > writable). There is no point do "debianize" Isabelle: it is a plain user-space application program, not a system component. You should be able to achive the above without deb packaging like this: * unpack the Isabelle tar.gz * run "Isabelle/bin/isabelle build -s -b HOL" (or any other images that users might need) * copy the result to the target (e.g. via "cp -a" or as a tar.gz) Here "Isabelle" refers to any Isabelle distribution from recent years: it is normal that Isabelle users have more than one of it active. Also note that "isabelle build" uses SHA1 hash keys on the sources, not datestamps. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts
On 24/11/2018 19:51, Makarius wrote: > *** General *** > > * The font family "Isabelle DejaVu" is systematically derived from the > existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" > and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique". > The DejaVu base fonts are retricted to well-defined Unicode ranges and > augmented by special Isabelle symbols, taken from the former > "IsabelleText" font (which is no longer provided separately). Side-remark: this works via "isabelle build_fonts -d dejavu-fonts-ttf-2.37/ttf" The Isabelle/Scala sources of this tool should be obvious, see http://isabelle.in.tum.de/repos/isabelle/file/395c4fb15ea2/src/Pure/Admin/build_fonts.scala In the past, people have occasionally pointed out that the standard Isabelle font is a bit boring. If there are other high-quality fonts to be considered for the Isabelle font portfolio, I am interested to hear about them. Of course, it is also possible to use private Isabelle-derivatives of existing fonts, such as some Apple fonts that are provided with macOS. (These are usually non-free and we cannot ship them by default.) It is generally better to have all special glyphs in a single font where all sizes are carefully fit together, instead of implicit or explicit multi-font assembly in GUI frameworks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Isabelle DejaVu fonts
*** General *** * The font family "Isabelle DejaVu" is systematically derived from the existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique". The DejaVu base fonts are retricted to well-defined Unicode ranges and augmented by special Isabelle symbols, taken from the former "IsabelleText" font (which is no longer provided separately). The line metrics and overall rendering quality is closer to original DejaVu. INCOMPATIBILITY with display configuration expecting the old "IsabelleText" font: use e.g. "Isabelle DejaVu Sans Mono" instead. * The Isabelle fonts render "¯" properly as superscript "-1". *** Isabelle/jEdit Prover IDE *** * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle DejaVu" collection by default, which provides uniform rendering quality with the usual Isabelle symbols. For Java/Swing GUI elements this requires the Metal look-and-feel: it is the default on Linux, but not macOS nor Windows. Line spacing no longer needs to be adjusted: properties for the old IsabelleText font had "Global Options / Text Area / Extra vertical line spacing (in pixels): -2", now it defaults to 0. * Improved sub-pixel font rendering (especially on Linux), thanks to OpenJDK 11. This refers to Isabelle/395c4fb15ea2 and Isabelle/6aa24ccd8049. The idea to construct Isabelle fonts systematically with the fontforge scripting language has been in the pipeline for a long time. It has now been flushed due to the change of font-rendering in the OpenJDK 11 version that we are using: now we have proper bold-italic fonts as well, which is relevant to render control symbols like \<^term>. I have taken the opportunity to brush-up the whole font setup, such that we are again a little better of than before, according to the strict monotonicity principle of Isabelle development. Users hooked on isabelle-dev versions might have to revisit their Isabelle/jEdit properties, to ensure that no "IsabelleText" font specifications are left. Already existing user properties take precedence over defaults provided by Isabelle/jEdit: see $ISABELLE_HOME_USER/jedit/properties vs. $ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props and recall that the "properties" file cannot be changed while Isabelle/jEdit is running (it will be overwritten on application shutdown). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] illegal reflective access
On 15/11/2018 22:13, Makarius wrote: > On 15/11/2018 19:44, Lawrence Paulson wrote: >> Got this upon launch. Is it important? >> >> 341ebf35464b tip >> >> WARNING: Illegal reflective access by macosx.MacOSXPlugin to method >> com.apple.eawt.FullScreenUtilities.setWindowCanFullScreen(java.awt.Window,boolean) >> WARNING: Please consider reporting this to the maintainers of >> macosx.MacOSXPlugin > > I am de-facto the maintainer of macosx.MacOSXPlugin -- see also > https://sourceforge.net/p/jedit/plugin-patches/186 > > Here I have overlooked the dynamic access to > com.apple.eawt.FullScreenUtilities -- it still needs to be sorted out. I did not find a way around this, even after looking at the Java 11 sources. Maybe it is not really required (which still needs to be tested on macOS), or there will be a replacement in a future Java release. For now we can just ignore this particular warning about FullScreenUtilities.setWindowCanFullScreen We can't ignore other warnings, though. In Isabelle/740b14b67472 I have added --illegal-access=warn to the default Java options: it means that warnings are not disabled after the first warning message. This can spam or bomb the system, but hopefully we don't have too many such unclear cases left over. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] illegal reflective access
On 15/11/2018 19:44, Lawrence Paulson wrote: > Got this upon launch. Is it important? > > 341ebf35464b tip > > WARNING: Illegal reflective access by macosx.MacOSXPlugin to method > com.apple.eawt.FullScreenUtilities.setWindowCanFullScreen(java.awt.Window,boolean) > WARNING: Please consider reporting this to the maintainers of > macosx.MacOSXPlugin I am de-facto the maintainer of macosx.MacOSXPlugin -- see also https://sourceforge.net/p/jedit/plugin-patches/186 Here I have overlooked the dynamic access to com.apple.eawt.FullScreenUtilities -- it still needs to be sorted out. Such warnings by Java 11 refer to internal things that will no longer be accessible in the near future -- Oracle started to robustify this with Java 9, and will become serious about it eventually. We need to eliminate such illegal accesses one-by-one, as they occur at run-time. Just today I've made a change in a different corner: changeset: 69301:5a71b5145201 user:wenzelm date:Wed Nov 14 21:43:33 2018 +0100 files: src/Pure/General/http.scala description: prefer statically-typed close operation, avoid Java 11 warning: "Illegal reflective access by scala.reflect.package$ to method sun.net.httpserver.LeftOverInputStream.close()"; There are more fine-points about OpenJDK 11 that are still to be discovered and sorted out. Only recently, I have noticed that the derived italic versions of the IsabelleText font don't work -- the current plan is to use fontforge to make a proper font instead. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala
On 11/11/2018 16:44, Lars Hupel wrote: >> * Support for Isabelle command-line tools defined in Isabelle/Scala. >> Instances of class Isabelle_Scala_Tools may be configured via the shell >> function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle >> component). > > This is nice! Anything on the radar to automate compilation as well, > just like `jedit -bf`, but for arbitrary components? That would be very > useful for the AFP. I know, and I've (re)started thinking about it. Somehow there should be a mechanism to augment the Admin/build process in user-space. It would also mean to get rid of the special "isabelle jedit -b" in various situations of system initialization. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala
*** System ***
* Support for Isabelle command-line tools defined in Isabelle/Scala.
Instances of class Isabelle_Scala_Tools may be configured via the shell
function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
component).
This refers to Isabelle/258bef08b31e. In recent years we have seen a
trend to use proper Isabelle/Scala instead of odd scripts (Bash, Perl,
Python etc.). Now it is possible to do this for user-space components
that provide their own classpath jars with instances of class
Isabelle_Scala_Tools. So far this only worked for .scala scripts, which
where interpreted.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 08/11/2018 21:32, Makarius wrote:
> Over the decades we have accumulated funny quotation forms in Isabelle
> syntax that are often hard to explain to new users (also to old users).
I don't have a full overview of all the fine points yet, but the general
idea is like this:
* cartouches are the main mechanism to embed/nest languages, e.g.
outer syntax -> document source -> inner syntax -> formal comment ->
antiquotation -> ...
* retain " ... " as a way to quote names and other small bits of text;
its main use to embed inner syntax might eventually be superseded by
cartouches (which some users already do routinely)
* keep the status-quo of (* ... *) as outer comments (source text that
is not part of the document)
The following can be probably phased out right now:
* verbatim quotations {* ... *}
* alt_string `...`
Both become cartouches; this is done by "isabelle update_cartouches"
already.
Rather soon there should be more advanced maintenance tools based on
semantic PIDE markup. E.g. it would allow to replace deeply nested
quotations reliably thanks to formal markup, say as a type/term within
ML. It would also allow to replace ":" by "\" systematically, when
that is formal notation of the term language.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 09/11/2018 00:08, gerwin.kl...@data61.csiro.au wrote: > We probably still have a few occurrences of these, but no problem > phasing them out. In principle it is just a matter of applying "isabelle update_cartouches -t", but it might require some coordination, especially on AFP. E.g. one could set a date for the "big sweep" and make one big changeset, or one could gradually update entries in an erratic manner. You can probably say better if there are problems to be expected between the "stable" and "devel" versions of AFP. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 09/11/2018 00:03, Peter Lammich wrote:
> I sometimes see {* *} in old theory files, and find it funny to be
> reminded that this was standard only 5 years ago ... from my side there
> are no uses of this quotation remaining that I'd know of
Indeed. Do you want to apply "isabelle update_cartouches" yourself on
various AFP entries, e.g. the Automatic_Refinement stack?
> However, (* *) is still very important for informally andquickly
> commenting things out, also in inner syntax!
That is only a historic footnote. It was actually very confusing to have
the same notation (* ... *) in two different meanings:
* outer syntax: material that is not part of the formal document, but
treated like white space; exception: slightly odd meta-comments (*<*)
... (*>*)
* inner syntax: material that is not considered part of the term
language, but shown in the document source in the text style of the term
language
At some point there will more Prover IDE support to add/remove the
various formal comments (with control symbols and cartouches) that have
emerged recently. But the old inner syntax is not coming back.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
On 08/11/2018 21:36, Lawrence Paulson wrote:
>> On 8 Nov 2018, at 20:32, Makarius wrote:
>>
>> In particular, what are the remaining uses of {* ... *}?
>
> I didn’t even know that existed.
It was used a lot with the 'section' and 'text' commands until recently.
That was actually its main motivation approx. 20 years ago: to delimit
LaTeX sources reliably.
Now the occurrence of {* ... *} in some existing sources makes them look
very old-fashioned, but "isabelle update_cartouches -t" does a thorough
job automatically.
> But I use (*...*) to enclose arbitrary text or comment material out.
Outer comment syntax will remain unchanged: its main purpose is to
comment-out material temporarily, or to write meta-comments (like % in
LaTeX).
Proper document text would normally appear within cartouches and marked
by 'text' or \.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Remaining uses of {* ... *} quotation?
Over the decades we have accumulated funny quotation forms in Isabelle
syntax that are often hard to explain to new users (also to old users).
In particular, what are the remaining uses of {* ... *}?
It should already be superseded by cartouches. There is also "isabelle
update_cartouches" to get rid of it (as well as `alt_string`).
The long-term trend is to converge to cartouches or double-quotes almost
everywhere. Cartouches are for nested languages, and double quotes for
string literals or names that are in conflict with other syntax.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
This is the updated situation according to Isabelle/c1a27fce2076: *** System *** * Support for managed installations of Glasgow Haskell Compiler and OCaml via the following command-line tools: isabelle ghc_setup isabelle ghc_stack isabelle ocaml_setup isabelle ocaml_opam The global installation state is determined by the following settings (and corresponding directory contents): ISABELLE_STACK_ROOT ISABELLE_STACK_RESOLVER ISABELLE_GHC_VERSION ISABELLE_OPAM_ROOT ISABELLE_OCAML_VERSION After setup, the following Isabelle settings are automatically redirected (overriding existing user settings): ISABELLE_GHC ISABELLE_OCAML ISABELLE_OCAMLC The old meaning of these settings as locally installed executables may be recovered by purging the directories ISABELLE_STACK_ROOT / ISABELLE_OPAM_ROOT. I have also started experimenting with the following in $ISABELLE_HOME_USER/etc/settings: ISABELLE_STACK_ROOT="$HOME/.stack" ISABELLE_OPAM_ROOT="$HOME/.opam" The Isabelle scripts should ensure that the specified versions are used, independently of other versions that a user might have installed already. In any case, both "stack" and "opam" stack-up considerable material: it is easy to fill 5-15 GB of disk space after working some time. Only docker requires even more space. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
On 08/11/2018 14:59, Bertram Felgenhauer wrote: >> >> I've misunderstood the problem. You intend to invoke old-style >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. > > This may be premature, but I foresee that now that `isabelle ghc` > and `isabelle ghci` exist, we will have scripts that use them. There is indeed some confusion here. My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained by the odd recursive setup: in the stack situation, $ISABELLE_GHC points to lib/Tools/ghc, and some mistake in the configuration could lead to infinite recursion of sub-processes (potential bombing of the OS). It is probably better to leave the meaning of ISABELLE_GHC (and ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle ghc" tool entry points: these auxiliary scripts should go into $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular Isabelle tools. I have now also learned that "ghci" is just "ghc --interactive", so there is no point to treat it too prominently. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
On 08/11/2018 12:16, Makarius wrote: > On 08/11/2018 11:30, Bertram Felgenhauer wrote: >> Makarius wrote: >>> Nonetheless, it is still possible to use "isabelle ghc" without stack: >>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the >>> Isabelle settings mechanism to override ISABELLE_GHC with the >>> stack-based tools. >> >> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about >> a missing GHC setup, since there's no fallback on a custom >> $ISABELLE_GHC. I've added such a fallback in the attached patch, >> does that look reasonable? > > I've misunderstood the problem. You intend to invoke old-style > $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. > > So just the usual question: What are remaining uses of this? Why not > uninstall the "system ghc" and only use stack? It should be possible to > direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting > out remaining problems on that side. > > My impression is that up-to-date Haskell projects are all using stack by > default. A remaining use of "unmanaged" ghc is actually ocaml: I would like to keep these tools as uniform as possible, see also current a41f49148525. Unfortunately, OPAM is not as advanced as stack yet, e.g. it does not quite work on Windows so the Cygwin ocaml is still needed. We could move the other way and discontinue the meaning of $ISABELLE_GHC and $ISABELLE_OCAMLC as actual executables: the settings would merely indicate the presence of these tools, e.g. for options [condition = ISABELLE_GHC] in session ROOT entries. It probably would require some changes of the Codegen setup, because that wants to see a single environment variable instead of a command-line fragment like "isabelle ghc" or "isabelle ocamlc". Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
On 08/11/2018 11:30, Bertram Felgenhauer wrote: > Makarius wrote: >> Nonetheless, it is still possible to use "isabelle ghc" without stack: >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the >> Isabelle settings mechanism to override ISABELLE_GHC with the >> stack-based tools. > > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about > a missing GHC setup, since there's no fallback on a custom > $ISABELLE_GHC. I've added such a fallback in the attached patch, > does that look reasonable? I've misunderstood the problem. You intend to invoke old-style $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. So just the usual question: What are remaining uses of this? Why not uninstall the "system ghc" and only use stack? It should be possible to direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting out remaining problems on that side. My impression is that up-to-date Haskell projects are all using stack by default. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Isabelle/PIDE modules for Haskell
*** System ***
* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some
source modules for Isabelle tools implemented in Haskell, notably for
Isabelle/PIDE.
This refers e.g. to current Isabelle/438e1a11445f.
There is more and more material emerging: as direct ports from
Isabelle/ML using the our canonical naming conventions and functional
programming style.
I writing these sources with VSCode and the extension "Haskell Language
Server" 0.0.24, see also https://github.com/haskell/haskell-ide-engine
After several days of tinkering it now works fairly well for me, even
with friendly hints via hlint. Unfortunately I failed to reproduce the
installation on my mobile machine. This reminds a bit of ancient times
with vi and emacs, before Isabelle/PIDE/jEdit.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
On 07/11/2018 16:32, Bertram Felgenhauer wrote: > Makarius wrote: >> *** System *** >> >> * Support for Glasgow Haskell Compiler via command-line tools "isabelle >> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack". >> Existing settings variable ISABELLE_GHC is maintained dynamically >> according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER. >> >> >> This refers to Isabelle/1722cc56d22e. > > Is there a way to use a system ghc with `isabelle ghc` and > `isabelle ghci`? I want to avoid the 145MB download and extra > installation of ghc if possible. The directory $ISABELLE_STACK_ROOT should be actually somewhat bigger: up to 5 GB for all the library modules. On Windows there is another directory to take care of, according to "stack path programs". I do prefer using up disk space and get a well-defined installation in return. (I am presently working with someone building a Haskell-based tool that is connected to Isabelle: the very first problem we had to overcome was "cabal dependency hell". With stack it worked out nicely on the spot, even on Windows and Mac OS X.) Nonetheless, it is still possible to use "isabelle ghc" without stack: you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the Isabelle settings mechanism to override ISABELLE_GHC with the stack-based tools. > Note in particular that setting ISABELLE_GHC now has a peculiar > effect on `isabelle ghc`. Without the environment variable, the > command complains: > > Cannot execute ghc: missing Isabelle GHC setup > > However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings, > then the same command starts downloading ghc via stack... This should be more robust in current Isabelle/8bfa615ddde4 (the relevant change is c911716d29bb). You need to run "isabelle ghc_setup" once again to ensure that the extra file "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" is present -- otherwise it will fall back on old-style ISABELLE_GHC defaults despite the presence of $ISABELLE_STACK_ROOT. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jdk-11
On 13/10/2018 22:39, Makarius wrote: >> >> I've quickly tried openjdk-11 on Ubuntu 18.10 beta: the same low-grade >> font rendering. It is particularly bad in Isabelle/jEdit file-open dialog. > > Thanks to a useful hint by the "Felix von Leitner Institute for > distributed real-time Java" I've found the following alternative: > https://adoptopenjdk.net > > It looks much better on Linux, even with subpixel antialiasing. > > I will make a new component from it when the next Java 11 update is > released. Java 11.0.1 has been released by Oracle, but https://adoptopenjdk.net appears to have its own release scheme: it is still on jdk-11+28 from Aug-2018. So I have updated the jdk and jedit-build components right now: see Isabelle/f714114b0571. It should work smoothly on all platforms, even on macOS: I have updated the MacOSX plugin accordingly and bundled it with Isabelle as before (when that gets updated officially by the jEdit project, it might cause some confusion, though). The font-rendering of this OpenJDK version is quite different from what we've seen from Oracle since Java 7. The Isabelle font is a bit thinner than before, but sub-pixel rendering works better, especially on Linux. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
On 22/10/2018 15:05, Lars Hupel wrote: > > I'm trying out a High Sierra Mac Book Pro, and Stack appears to work there. > > Interestingly enough, I get Poly/ML warnings of the form: > > 14:11:19 poly(50366,0xb042) malloc: *** mach_vm_map(size=8388608) > failed (error code=3) > 14:11:19 *** error: can't allocate region > 14:11:19 *** set a breakpoint in malloc_error_break to debug > > This happens during the build of "HOL-Decision_Procs", which succeeds > regardless: > > 14:11:19 Finished HOL-Decision_Procs (0:05:36 elapsed time, 0:10:40 cpu > time, factor 1.91) This is a normal feature of memory management on macOS. After all these years, David Matthews might eventually want to look if it is still required these days: for that he merely needs regular SSH access to some test machine. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
