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] 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
[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
[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
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
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 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] 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] 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] 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 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] 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
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
[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
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] 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
[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] 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] 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] 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 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/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] 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] 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] 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] 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] 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 (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] 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 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
[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: 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
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: 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 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: 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 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
[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] 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
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] 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] 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] 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] 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
[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] 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
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
[isabelle-dev] position of Hilbert_Choice in the HOL theory hierarchy
On Fri, 14 Sep 2007, Stefan Berghofer wrote: For those members of the list who have not followed the discussion about this issue a few years ago, let me cite what Larry wrote about it: I think it would be quite easy to do, and sensible (ZF has always been that way). [...] If the necessary effort is reasonable, it would be nice to remove AC from the core. It has a corrupting influence. For example, somebody generalized Least to LeastM, which at first sight is a natural generalization, but LeastM requires AC while Least does not. In my opinion, a theory that does not depend on any unnecessarily strong axioms also seems to be more appealing from a foundational point of view. I agree with this. Makarius
[isabelle-dev] NEWS
* ML basics: just one true type int, which coincides with IntInf.int (even on SML/NJ).
[isabelle-dev] NEWS
* Pure/Isar: unified syntax for new-style specification mechanisms (e.g. 'definition', 'abbreviation', or 'inductive' in HOL) admits full type inference and dummy patterns (_). For example: definition K x _ = x
[isabelle-dev] NEWS
* ML/Isar: simplified interfaces for outer syntax. Renamed OuterSyntax.add_keywords to OuterSyntax.keywords. Removed OuterSyntax.add_parsers -- this functionality is now included in OuterSyntax.command etc. INCOMPATIBILITY.
[isabelle-dev] NEWS
* System: polyml-platform script now identifies x86_64-linux with x86-linux, which is usually more efficient. INCOMPATIBILITY, requires manual settings if x86_64-linux is really intended (e.g. for 2GB heap or 64MB stack).
[isabelle-dev] Isabelle sources at 0 Kelvin
Dear Isabelle contributors, as we approach the official Isabelle2007 release, the CVS has finally reached the critical point of 0 Kelvin (concerning entropy of the sources). This means that further changes to the main system and libraries will only be accepted if they address critical problems (show stoppers). There are still a couple of days left to polish the manuals, though. Due to the enormous complexity of the system with all its contributing components (Proof General, Poly/ML, external provers etc.) and the multitude of supported platforms, we still need something like two weeks of testing until the final release can be shipped. See http://www4.in.tum.de/~wenzelm/test/website-test/index.html for the present snapshot, which is called isa2007-test instead of the forthcoming Isabelle2007. Please take the opportunity to check this on your favourite system installation (homegrown Linux kernel, exotic Emacs version etc.), using the official binaries provided from the website. Makarius
[isabelle-dev] NEWS
On Sun, 6 Jan 2008, Makarius wrote: * Rudimentary Isabelle plugin for jEdit (see Isabelle/lib/jedit), based on Isabelle/JVM process wrapper (see Isabelle/lib/classes). Note that the precompiled jars are only available in a proper distribution, but not in the internal CVS (cf. Admin/makedist). There has been a problem with makedist on sunbroy2, which is used by isatest. So I've disable compilation of the jEdit plugin for the time being -- until I come back from vacation in two weeks. Just in case anybody wants to try it out anyway, see http://www4.in.tum.de/~wenzelm/test/Isabelle_06-Jan-2008.tar.gz Makarius
[isabelle-dev] NEWS
* Theory loader: use_thy (and similar operations) no longer set the implicit ML context, which was occasionally hard to predict and in conflict with concurrency. INCOMPATIBILITY, use ML within Isar which provides a proper context already.
[isabelle-dev] record pretty printing
On Wed, 13 Feb 2008, Gerwin Klein wrote:
What does work is replacing it by \\^constProduct_Type.Unity, but
that feels very ad-hoc to me (I'm not sure where the \^const comes
from), so I haven't committed it yet.
The SML antiquotation @{const_syntax Unity} should do the trick.
Makarius
[isabelle-dev] NEWS (update)
* Eliminated theory ProtoPure and CPure, leaving just one Pure theory. INCOMPATIBILITY, object-logics depending on former Pure require additional setup PureThy.old_appl_syntax_setup; object-logics depending on former CPure need to refer to Pure.
[isabelle-dev] NEWS
* ML: rules and tactics that read instantiations (read_instantiate, res_inst_tac, thin_tac, subgoal_tac etc.) now demand a proper proof context, which is required for parsing and type-checking. Moreover, the variables are specified as plain indexnames, not string encodings thereof. INCOMPATIBILITY.
[isabelle-dev] NEWS
* ML: Disposed old term read functions (Sign.read_def_terms, Sign.read_term, Thm.read_def_cterms, Thm.read_cterm etc.). INCOMPATIBILITY, should use regular Syntax.read_term, Syntax.read_term_global etc.; see also OldGoals.read_term as last resort for legacy applications.
[isabelle-dev] HOL vs. HOL-Complex
On Wed, 2 Jul 2008, Brian Huffman wrote: The important point is that all the NSA stuff can be taken out without losing any real functionality, since we are still left with a complete development of *standard* analysis. That's very interesting to hear. Does it mean that there is no particular advantage in the NSA part anymore, unless you are specifically interested in the non-standard thing? Makarius
[isabelle-dev] NEWS (update)
* @{lemma} in latex and ML: allow initial and terminal method expressions,
as in the Isar command 'by'.
* @{lemma} in ML now closes the derivation, unless @{lemma (open) ...} is
specified.
[isabelle-dev] ProofGeneral history via Mercurial
Dear Mercurial enthusiasts and Proof General users, as ProofGeneral is heading towards the *stable* release 3.7.1 it might be interesting to follow the ongoing development via http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/atom-log Access to the regular repository also works via the parent directory of that URL. Note that this is a readonly copy of the official ProofGeneral CVS from Edinburgh. As usual, early adopters of PG pre-3.7.1 should post problem reports to http://proofgeneral.inf.ed.ac.uk/trac/ (you can just create your own account). Makarius
[isabelle-dev] NEWS
On Sun, 24 Aug 2008, Tobias Nipkow wrote: I don't have a lib subdirectory and cvs does not know about one. The NEWS are always in terms of a proper distributions, for users out there. The CVS layout is a bit mangled, and lib is in Distribution/lib. Makarius
[isabelle-dev] Fwd: Re: new isabelle interface
On Mon, 25 Aug 2008, Michael Nedzelsky wrote: I plan to use SML.NET to compile Isabelle. Does anyone forsee any problems with this? Is Isabelle's code fairly portable across Standard ML compilers? The SML.NET user manual says (p. 4). No interactive evaluation. The interactive environment is for compilation of stand-alone applications or libraries only. SML expressions can not be evaluated interactively and the use command is not available. Isabelle sources contains many use commands, so it will not run on SML.NET. This should settle that question. Runtime use of ML source is an inherent requirement of the LCF-style architecture of Isabelle. Building theories and corresponding proof tools etc. is an alternating process that never stops. Concerning the general architecture of UI vs. prover there is the fundamental choice of having everything in a single process vs. the Proof General way of speaking to a separate prover process via pipes. In Coq-IDE you have the first variant, where everything is in OCaml. This simplifies the implementation, because values can be passed between the prover and GUI without a separate protocol. On the other hand, I've heard from Coq users that Coq-IDE stability suffers signigicantly from joining the two parts in one process, and they want to traditional Proof General mode back. Since we do not really have the choice in Isabelle anyway (there is no real GUI support in Poly/ML), we can be glad to be on the right track already: keep with the separate process model. Apart from stability it also allows to run the prover and GUI an separate machines. (``Modern'' GUIs do need 1 or 2 cores for themselves, just to display things to the user.) Makarius
[isabelle-dev] new isabelle interface
On Mon, 25 Aug 2008, Cameron Freer wrote: One can type a single command from the SAGE commandline to spawn a local webserver running the notebook interface. I've found the AJAX interface to be surprisingly clean, responsive, and pleasant, even for those used to the commandline. Such a web interface for Isabelle would probably be more complicated, but it does offer similar advantages -- not just the ability to separate the kernel from the UI, but also portability (for users running it locally). Kaliszyk proposed something similar for Coq a couple years ago: http://www.easychair.org/FLoC-06/UITP-preproceedings.pdf#page=57 Very good. Cezary Kaliszyk is actually one of the prover UI people who greatly influenced the upcoming Isabelle architecture. Cezary has quite responsive AJAX / JavaScript on the client side, but on the server his own OCaml wrapper around the prover, which exposes a couple of problems. The latter can be easily replaced by a more robust version using the new Scala classes of Isabelle, using existing server tools available for the JVM. If there are any AJAX experts out there who would like to produce an interface to our (slowly emerging) server infrastructure, I would be happy to assist them. Makarius
[isabelle-dev] new isabelle interface
On Mon, 25 Aug 2008, Chris Capel wrote: The latest sources are always available via http://isabelle.in.tum.de/repos/isabelle/ which even allows you to subscribe to the changelog via RSS/Atom, so you can immerse yourself in tons of fine-grained change messages :-) You have mentioned CVS a few times, and yet that link refers to Mercurial. Is that a read-only mercurial mirror? Yes. There is a cron job that sucks the changes from the CVS every hour and adds them to the Mercurial repository. In principle one could push changes onto the latter, but there is no practical way to put them back into the CVS. We are still working on getting more Isabelle people aquainted with Mercurial, so that we can get rid of CVS eventually. Makarius
[isabelle-dev] isabelle/repos
Dear Mercurial enthusiasts, the URL for the Isabelle sources (still read-only) is now http://isabelle.in.tum.de/repos/isabelle/ The old http://isabelle.in.tum.de/isabelle-bin/mercurial.cgi/ will disappear soon. Adapting local clones of this repository merely involves editing the default path in .hg/hgrc -- unlike CVS/SVN the Mercurial meta data is only in a single place within each repository. Anybody who has not tried Mercurial yet should do so now. It is the kind of tool that makes live much easier, only at the cost of unlearning quirks of CVS/SVN. (The way of thinking needs to be de-centralized.) Makarius
[isabelle-dev] Relation_Power.thy
On Tue, 2 Sep 2008, David Aspinall wrote: \caret:funpow \caret:relpow This is already supported in the X-Symbol replacement in the CVS version of Proof General, by the way, although Isabelle's lexer currently only allows syntax like \caret1 and \caret2. The \symbol notation is more fundamental, below lexing even. It is actually fashioned after Java's \u for UTF-16 chars, but we do not depend on unicode encoding variants of course. You can achieve the above name space effect of symbols already via something like \caret_funpow, which is presently unused because LaTeX output is a bit strange (as for \caret1). This means \foo_bar and \foo42 are both unlikely to be used already for something else. There is also a more compositional way to produce symbol variants: \^control\symbol. Here nothing needs to be changed in Isabelle, only the UI needs to provide sane input methods and proper display (without the flashing of x-symbol for \^sub for example). Makarius
[isabelle-dev] NEWS
* Name bindings in higher specification mechanisms (notably LocalTheory.define, LocalTheory.note, and derived packages) are now formalized as type Name.binding, replacing old bstring. INCOMPATIBILITY, need to wrap strings via Name.binding function, see also Name.name_of. Packages should pass name bindings given by the user to underlying specification mechanisms; this enables precise tracking of source positions, for example.
[isabelle-dev] Mercurial conversion relaunch
On Wed, 3 Sep 2008, Makarius wrote: Within the next few hours http://isabelle.in.tum.de/repos/isabelle will recover to the present state of the CVS. Since this is a fresh Mercurial repository, local clones probably need to be recreated from scratch. In the mean tome it might be helpful to refer to the old version, now at http://isabelle.in.tum.de/repos/isabelle-old/ Makarius
[isabelle-dev] [Fwd: Re: Find]
On Fri, 12 Sep 2008, Tobias Nipkow wrote: Vermutlich spricht der Optimierer Deutsch und hat das in der letzten Woche optmiert - in der Version auf meinem Mac kommt auch noch der volle Name raus. Ideal waere die kuerzeste legale Abk. Tobias Original-Nachricht Betreff: Re: Find Datum: Fri, 12 Sep 2008 09:39:21 +1000 Von: Gerwin Klein gerwin.klein at nicta.com.au An: Tobias Nipkow nipkow at in.tum.de Referenzen: 48C92DF8.7000903 at in.tum.de Wir sind unschuldig, das mu? jemand optimiert haben. In unserer Version kommt immer der fully qualified name raus. Selbst wenn der kurze Name eindeutig ist, will man oft den langen, um rauszufinden aus welcher Theorie das Theorem kommt. Gerwin On 12/09/2008, at 0:40, Tobias Nipkow nipkow at in.tum.de wrote: gibt nur den Basisnamen eines Theorems aus. Das kann Probleme machen. Such mal nach fold _ _ _ (insert _ _), dann bekommst du 3 mal fold_insert, wobei das erste davon nur als ab_semigroup_mult.fold_insert ansprechbar ist. Mit der richtigen name space function muesste da der passend abgekuerzte Name rauskommen. Tobias It is a bit hard to follow this fragmentary stuff, nevertheless I managed to find the source of the presumed problem. Concerning my version, your version of the sources, we can do this properly once we have switched to Mercurial, because it provides unique version identifiers which other people can use to look up the very version precisely. Makarius
[isabelle-dev] NEWS
* The Isabelle emacs tool provides a specific interface to invoke Proof General / Emacs, with more explicit failure if that is not installed (the old isabelle-interface script silently falls back on isabelle-process). The PROOFGENERAL_HOME setting determines the installation location of the Proof General distribution. * The Isabelle System Manual (system) has been updated, with formally checked references as hyperlinks.
[isabelle-dev] [isabelle] Incompatibilities between releases (Re: Syntax for theory definitions)
On Sat, 27 Sep 2008, Florian Haftmann wrote: Proofs are much more fragile, notably unstructured ones. One way around this is to submit theory libraries and applications to http://afp.sourceforge.net/ where they get updated to latest Isabelle automagically. Thanks to all the magicians ;-) And the wizards ... Makarius
[isabelle-dev] Fwd: Broken link
On Wed, 1 Oct 2008, Lawrence Paulson wrote: In fact, all the links to logics in the theory library section are broken. I have fixed this problem of Isabelle2008 already, and said so recently in an answer to somebody on isabelle-users. Makarius
[isabelle-dev] NEWS
* Wrapper script for remote SystemOnTPTP service allows to use sledgehammer without local ATP installation (Vampire etc.). See also ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting variable. (By Fabian Immler, TUM) (CVS note: need to move Distribution/contrib/ out of the way, if it exists already locally.)
[isabelle-dev] NEWS
* Simplified main Isabelle executables, with less surprises on case-insensitive file-systems (such as Mac OS). - The main Isabelle tool wrapper is now called isabelle instead of isatool. - The former isabelle alias for isabelle-process has been removed (should rarely occur to regular users). - The Isabelle alias for isabelle-interface has been removed. Within scripts and make files, the Isabelle environment variables ISABELLE_TOOL and ISABELLE_PROCESS replace old ISATOOL and ISABELLE, respectively. (The latter are still available as legacy feature.) Also note that user interfaces are now better wrapped as regular Isabelle tools instead of using the special isabelle-interface wrapper (which can be confusing if the interface is uninstalled or changed otherwise). See isabelle tty and isabelle emacs for contemporary examples. INCOMPATIBILITY, need to adapt derivative scripts. Users may need to purge installed copies of Isabelle executables and re-run isabelle install -p ..., or use symlinks.
[isabelle-dev] NEWS
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
hypotheses. Sorts required in the course of reasoning need to be
covered by the constraints in the initial statement, completed by the
type instance information of the background theory. Non-trivial sort
hypotheses, which rarely occur in practice, may be specified via
vacuous propositions of the form SORT_CONSTRAIN('a::c). For example:
lemma assumes SORT_CONSTRAINT('a::empty) shows False ...
The result contains an implicit sort hypotheses as before --
SORT_CONSTRAINT premises are eliminated as part of the canonical
rule normalization.
[isabelle-dev] Multicore performance preview
On Tue, 21 Oct 2008, Stefan Berghofer wrote: Makarius wrote: You will need the latest Poly/ML 5.2.1 version to prevent a strange GC deadlock problem in 5.1/5.2. Where can I get the latest version? The latest version offered for download on the Sourceforge page http://sourceforge.net/project/showfiles.php?group_id=148318package_id=163589 is still 5.2 You are right, 5.2.1 has not been published yet. The present CVS version is more or less at the same state, see e.g. our /home/polyml/polyml-cvs/. Makarius
[isabelle-dev] [polyml] Release 5.2.1 (fwd)
Our usual packages for use with Isabelle are available here: http://isabelle.in.tum.de/polyml-5.2.1/ For any serious use of multithreading in recent development snapshots Poly/ML 5.2.1 is really required, but there is no immediate need to recompile the official Isabelle2008. Makarius -- Forwarded message -- Date: Wed, 22 Oct 2008 20:10:34 +0100 From: David Matthews david.matth...@prolingua.co.uk To: PolyML mailing list polyml at inf.ed.ac.uk Subject: [polyml] Release 5.2.1 I've now released version 5.2.1 of Poly/ML on the SourceForge site. This is largely a bug-fix release of 5.2 and incorporates various fixes to the run-time system and basis library. I'll update the release notes on the web site with details of the bug fixes. The functional IO library has been largely rewritten to be much more efficient. One change that may affect a few people is that X-Windows/Motif support is now turned off by default in the configure script. To include support for X-Windows/Motif specify --with-x when running configure Note: Since the compiler has not changed when you run Poly/ML 5.2.1 the start-up line will still say Poly/ML 5.2 Release. However poly -v will say something like Poly/ML 5.2 ReleaseRTS version: I386-5.2.1 David ___ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
[isabelle-dev] NEWS (update)
* Multithreading for Poly/ML 5.1/5.2 is no longer supported, only for Poly/ML 5.2.1 or later.
[isabelle-dev] NEWS
* The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the old ~/isabelle, which was slightly non-standard and apt cause surprises on case-insensitive file-systems, or when working with local copies of the Isabelle repository. INCOMPATIBILITY, need to move existing ~/isabelle/etc, ~/isabelle/heaps, ~/isabelle/browser_info to the new place. Special care is required when using older releases of Isabelle. Note that ISABELLE_HOME_USER can be changed in Isabelle/etc/settings of any Isabelle distribution.
[isabelle-dev] Isabelle on Mercurial
After several months of getting acquainted with distributed version control in general, we should be finally ready to switch the official Isabelle repository to Mercurial. In fact, http://isabelle.in.tum.de/repos/isabelle has been around in the present form for several weeks already. It can already be cloned right now, e.g. like this: hg clone http://isabelle.in.tum.de/repos/isabelle Further instructions are in http://isabelle.in.tum.de/repos/isabelle/file/tip/README_REPOSITORY Write access to the corresponding pull/push file space is not enabled yet, and we still have the automated conversion job that feeds changes from the old Isabelle CVS into the Mercurial repository. After pressing the red button, the conversion job will be stopped and pushing enabled. If anybody has significant amounts of uncommitted CVS changes in the pipeline, please say so now. In principle, one could have both repositories active for a few days, and merge later using means of Mercurial, but things should be kept as simple as possible. Makarius
[isabelle-dev] Netbeans 6.5 and Scala
For those working with Scala (which is more and more becoming an important part in Isabelle interfaces to the outside world) it might be interesting to get the latest Netbeans 6.5 released today: http://www.netbeans.org/downloads/index.html The excellent Scala plugin is not yet part of the official Netbeans repository yet, but see here http://blogtrader.net/page/dcaoyuan/entry/new_scala_plugin_for_netbeans This description is for 6.5 RC2 and works for 6.5 final unchanged. The plugin uses the current Scala 2.7.2.final. Makarius
[isabelle-dev] Directory layout
On Mon, 1 Dec 2008, Florian Haftmann wrote:
The switch to hg makes it possible to adapt some file locations (file
names) in the Isabelle distribution which have evolved over time but do
not fit to the logical structure of the distribution any longer,
according to the following table:
src/Provers/* ~ src/Tools/*
src/Pure/Tools/* ~ src/Tools/*
src/HOL/arith_data.ML ~ src/HOL/Tools
src/HOL/hologic.ML ~ src/HOL/Tools
src/HOL/simpdata.ML ~ src/HOL/Tools
I cannot really say much about HOL, you know better about its logical
structure.
Concerning src/Provers, src/Tools, src/Pure/Tools:
* The distinction of src/Provers and src/Tools is mostly nostalgic, so
Provers should go into Tools. For quite some time, we have already
followed the convention of putting new things in src/Tools.
* The role of src/Pure/Tools is still unclear. The difference is that
these are actually loaded into the Pure image, and all its
contributing sources should be in src/Pure. I would say we leave
src/Pure/Tools unchanged for now until we get a better idea.
BTW, moving files will also affect manuals. In the newer ones (isar-ref,
system, implementation) I have already used the @{file} document
antiquotation to get a statically checked references to the Isabelle file
space.
Makarius
[isabelle-dev] Isabelle on Mercurial
A few more tips on getting started in a safe way, and avoiding surprises: * Use hg outgoing to see beforehand what hg push would do; the same works for hg incoming and hg pull. There is a real danger of messing up our central push area by merging it with my earlier attempt of the CVS - hg conversion, which I had to discontinue some months ago. If you still happen to have a clone around on your machine, delete it now! * An easy way to protect against gross mistakes is to install the following hook in your ~/.hgrc on the home directory at TUM: [hooks] pretxnchangegroup = /home/isabelle-repository/repos/sanity-check The sanity check prevents pushes that are unusually big, or consist of a large number of changesets -- as in the above case of merging with the bogus version of the old Isabelle repository. This hook is installed in /home/isabelle-repository/repos/.hg/hgrc already, but the Mercurial security model prevents its execution if you are not wenzelm. This is what the warning Not trusting file ... refers to. Makarius
[isabelle-dev] NEWS (update)
On Tue, 2 Dec 2008, Tjark Weber wrote: On Sun, 2008-11-30 at 14:08 +0100, Makarius wrote: The old isabelle-interface wrapper could react in confusing ways if the interface was uninstalled or changed otherwise. Individual interface tool configuration is now more explicit, see also the Isabelle system manual. In particular, Proof General is now available via isabelle emacs. I am using the repository version of Isabelle, ProofGeneral-3.7.1-1.noarch.rpm, and GNU Emacs 22.2.1 (available as emacs or emacs-22.2). isabelle emacs yields /usr/share/ProofGeneral/isar/interface: line 233: exec: emacs22: not found This seems to be caused by PROOFGENERAL_EMACS= $(choosefrom /Applications/Emacs.app/Contents/MacOS/Emacs emacs22) in isabelle/etc/settings (line 202). Or is anything wrong with my configuration? You can either pass option -p emacs (or whatever that emacs executable is called on your system) or set PROOFGENERAL_EMACS in ~/.isabelle/etc/settings Makarius
[isabelle-dev] NEWS
On Tue, 2 Dec 2008, Tjark Weber wrote: On Sun, 2008-11-30 at 13:03 +0100, Makarius wrote: * The default for ISABELLE_HOME_USER is now ~/.isabelle instead of the old ~/isabelle, which was slightly non-standard and apt cause surprises on case-insensitive file-systems, or when working with local copies of the Isabelle repository. I am using the repository version of Isabelle. BTW, thanks to Mercurial you can now refer to the actual version you are using, by means of the unique changeset id. (This might be important in a less trivial situation, because the repository is in continues flow.) Despite isabelle getenv -a reporting ISABELLE_HOME_USER=/home/weber/.isabelle ISABELLE_OUTPUT=/home/weber/.isabelle/heaps//polyml-5.2_x86-linux the command ./build Pure creates a heap file in /home/weber/isabelle/heaps/polyml-5.2_x86-linux (Note the missing ..) Am I doing something wrong? This is right. The build script produces heaps for the distribution which is your repository clone here, which appears to be ~/isabelle In fact, one reason for the change of ISABELLE_HOME_USER=$HOME/.isabelle with the dot was to avoid a clash in excactly this situation. Now your user config directory and distribution directory are clearly separated. Of course, heaps produced inside the repository file space like that must not be committed. Makarius
[isabelle-dev] NEWS
On Wed, 3 Dec 2008, Gerwin Klein wrote: Makarius wrote: Of course, heaps produced inside the repository file space like that must not be committed. We might want to add an .hgignore file and put ^heaps/ in it. This should at least make accidental commits less likely. It is already there, together with some other things that people tend to commit by accident: syntax: glob *~ *.class *.jar .DS_Store syntax: regexp ^heaps/ ^browser_info/ ... In fact, accidental commits are not yet a desaster, because they are local only and can be repaired. Only an actual push will make things last forever. Makarius
[isabelle-dev] Isabelle on Mercurial
On Tue, 2 Dec 2008, Tjark Weber wrote: One can argue that such keys are not necessary (since files in the repository can be identified by their changeset id); however, this is true only as long as one knows where a file is coming from. If you want keyword expansion, instructions can be found here: http://www.selenic.com/mercurial/wiki/index.cgi/KeywordExtension This is only a retro feature, which comes with its problems. With Mercurial you have the whole history always around, and there is no need to encode (tiny) parts of it in the file. Before source control systems came about, people where used to have much more history on board. Note that recent GNU Emacs will happily tell you the file id of the current buffer, if available. Other tools like Netbeans also have substantial hg support built into the editing environment. The present plan about the old $Id$ artifacts is to remove them gradually, or just ignore them for now. Makarius
[isabelle-dev] Isabelle on Mercurial
One more general note getting started with Mercurial: When exploring features of the system, please do it privately, on smaller repositories first! The Isabelle repository is very complex and many other people depend on it working smoothly. Anything that might end up in the central place should be done with great care. Makarius
[isabelle-dev] Isabelle on Mercurial
On Tue, 2 Dec 2008, Tjark Weber wrote: On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote: With Mercurial you have the whole history always around, and there is no need to encode (tiny) parts of it in the file. Certainly $Id$ keys are rather useless as long as the file is part of a managed repository. However, files escape into the wild. In that case you would also have to add a checksum to make sure that the identification is actually correct, and require tools to check that fact. Mercurial does exactly that for you, and more. Note that Isabelle development snapshots also carry a Mercurial id already, and official releases can be mapped to an id via the release tag. Trouble starts when people tear distributions apart, but you cannot protect against everything. For now it is most important to get people acquainted with the new environment, and refrain from any complications that are not really necessary. I recommend to use the system mainly for everyday things now, i.e. the same kind of things that would have been done last week with CVS, and not try out all the potentially cool things right now (at least not on the Isabelle repository). Makarius
[isabelle-dev] Isabelle on Mercurial
On Wed, 3 Dec 2008, Gerwin Klein wrote: I'm no great friend of $Id$, but Tjark does have a point: we release development snapshots and it is very easy to confuse versions when people ask questions about specific files etc. People should be able to say which release they are using. For the development snapshot the release name is the id of the changeset that makedist encountered as tip. If anybody uses the repository directly, not a release, then hg tip will provide that information. Makarius
[isabelle-dev] Usage Isabelle2007
On Fri, 5 Dec 2008, Hakobyan Lilit wrote: ?Starting process? isabelle home/Isabelle2007/bin/isabelle-process -PI -m PGASCII HOL After this? nothing happens and when I try to use any? other command? I get? Proof process busy. Can you run the isabelle process from a plain tty, without Proof General in between? You can also try an older version of Proof General, e.g. http://isabelle.in.tum.de/dist-Isabelle2007/contrib/ProofGeneral-3.7pre071112.tar.gz The same in Isabelle2008 works alright, though, but I need the 2007 version. I am using Linux 64-bitIsabelle2007?polyml-5.2 ProofGeneral-3.7.1 Normally there is no need to use the 64 bit version, unless you have something like 8 GB of real memory. The 32 bit version is a bit faster. Makarius
[isabelle-dev] ISABELLE_HOME/contrib vs. ISABELLE_HOME/..
One hint on organizing local repository clones, and use them as (pseudo) distributions. Basically the default settings expect contributing components (polyml, ProofGeneral, etc.) either in ISABELLE_HOME/contrib or ISABELLE_HOME/.. This means one can easily avoid adding stuff to contrib inside the repos, where Mercurial will mark it as alien ?. Moreover, the same contrib components can be shared by multiple clones. # various clones of http://isabelle.in.tum.de/repos/isabelle ~/isabelle/repos ~/isabelle/repos-foo ~/isabelle/repos-bar # contrib stuff ~/isabelle/polyml ~/isabelle/ProofGeneral ~/isabelle/E ... With this layout there is no need to edit ~/.isabelle/etc/settings or create symlink etc. Makarius
[isabelle-dev] TortoiseHg: GUI for Mercurial
Another hint on add-on tools for Mercurial. TortoiseHg http://tortoisehg.sourceforge.net/ is a nice graphical interface for Mercurial. For historical reasons it is advertized mostly for windows, but it also works for Linux and Mac OS, using a generic Python/Gtk application http://tortoisehg.wiki.sourceforge.net/hgtk For example, the hgtk log tool is similar to the old hg view (which was a bit ugly due to Tcl/Tk). Makarius
[isabelle-dev] NEWS
* HOL: command 'atp_messages' displays recent messages issued by automated theorem provers. This allows to examine results that might have got lost due to the asynchronous nature of default 'sledgehammer' output. (This acknowledges the fact that sledghammer occasionally breaks the Proof General model, which is inherently synchronous.)
