Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

2019-03-14 Thread Makarius
evil in some sense. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

2019-03-14 Thread Makarius
Here "admin" means: run outside of Isabelle in sequential mode. 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

2019-03-14 Thread Makarius
e 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

Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma

2019-03-14 Thread Makarius
ve had this discussion some month ago concerning stack: it is just too heavy to be the only way to refer to ghc). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

2019-03-13 Thread Makarius
l 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 mailin

Re: [isabelle-dev] NEWS

2019-03-13 Thread Makarius
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. >> >>

Re: [isabelle-dev] NEWS

2019-03-13 Thread Makarius
m Export/Generated_Files in ML for the 'codegen' command in particular. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: Update to Poly/ML 5.8 -- and towards Isabelle2019

2019-03-12 Thread Makarius
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

[isabelle-dev] NEWS: option system_heaps

2019-03-01 Thread Makarius
NCOMPATIBILITY 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/pref

Re: [isabelle-dev] Creating Theorems in ML

2019-02-28 Thread Makarius
ion.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.informa

Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2

2019-02-24 Thread Makarius
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 >> b

Re: [isabelle-dev] Towards Poly/ML 5.8

2019-02-23 Thread Makarius
nt to break the persistent data model just to be fully up-to-date at the "tip" version. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Makarius
o >> >> 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.in

Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2

2019-02-22 Thread Makarius
icode 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

2019-02-22 Thread Makarius
ely 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] Towards Poly/ML 5.8

2019-02-20 Thread Makarius
much less resources). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] polyml-test-8fda4fd22441 available for testing

2019-02-17 Thread Makarius
to be tested thoroughly, of course. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-16 Thread Makarius
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

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-14 Thread Makarius
e 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 _

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-14 Thread Makarius
aybe 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

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-13 Thread Makarius
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: > > *

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-13 Thread Makarius
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

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-10 Thread Makarius
and the latter sources always require extra work to locate.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-10 Thread Makarius
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

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-10 Thread Makarius
ine. We are (very slowly) moving towards the Isabelle2019 release (presumably June 2019), and everything needs to be beyond doubt when released. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-10 Thread Makarius
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. >

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-05 Thread Makarius
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

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

2019-02-05 Thread Makarius
heap: 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

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-05 Thread Makarius
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 ___ is

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-04 Thread Makarius
ces/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/Collect

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-04 Thread Makarius
dded support for executable exports in Isabelle/c175499a7537 -- a few more such fine-tunings might be required. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Uniform Isabelle repository clones via https://isabelle.sketis.net/repos

2019-02-04 Thread Makarius
(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

Re: [isabelle-dev] Timeouts in Flyspeck_Tame

2019-02-04 Thread Makarius
/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://mailma

Re: [isabelle-dev] Analysis not building

2019-02-02 Thread Makarius
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-1b2dc

Re: [isabelle-dev] Analysis not building

2019-02-02 Thread Makarius
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”. >> >> Th

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-02 Thread Makarius
g 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 on

Re: [isabelle-dev] Analysis not building

2019-02-02 Thread Makarius
rovements by David Matthews. After a standard test, I will probably make the above version the default again. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] polyml-test-b68438d33c69

2019-02-01 Thread Makarius
FP 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 ___ is

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-01 Thread Makarius
plemented in Haskell or OCaml should be particularly easy. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources

2019-02-01 Thread Makarius
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 "

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-01 Thread Makarius
y 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 ___

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-01 Thread Makarius
e 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

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-01 Thread Makarius
m to make them fit to the model. (This sometimes requires minor adjustments of the model.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources

2019-01-31 Thread Makarius
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:&

[isabelle-dev] NEWS: File Browser and Virtual File-systems for Isabelle resources

2019-01-31 Thread Makarius
entry. Since the latter is also under PIDE control, CTRL/COMMAND-MOUSE-HOVER-CLICK quickly leads to some theories. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: option "jedit_text_overview"

2019-01-31 Thread Makarius
s by extra GUI elements. (All other GUI elements had already options in jEdit or Isabelle). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-01-31 Thread Makarius
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

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-01-31 Thread Makarius
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 th

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-01-31 Thread Makarius
e "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

2019-01-31 Thread Makarius
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.

Re: [isabelle-dev] Question about testing isabelle with Poly/ML x86_64_32

2019-01-29 Thread Makarius
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

2019-01-27 Thread Makarius
er note that --gcthreads is automatically provided, if ML_OPTIONS does not say anything else. > 623083120 IsaFoR_2 (1.00) > 623291272 IsaFoR_2 (1.00) > 367497971 IsaFoR_2 (0.59) > 884213127 IsaFoR_2 (1.42) ? I have briefly tried IsaFoR_

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)

2019-01-25 Thread Makarius
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/45912

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing (polyml-test-a444f281ccec)

2019-01-23 Thread Makarius
in $ISASELLE_HOME_USER/etc/settings are cleaned up, such that this greatest and latest version gets used. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-23 Thread Makarius
nz_C0 (0:06:54 elapsed time, 0:50:34 cpu time, factor 7.33) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-23 Thread Makarius
On 23/01/2019 14:14, Bertram Felgenhauer wrote: > Makarius wrote: >> On 22/01/2019 12:31, Bertram Felgenhauer wrote: >>> Makarius wrote: >>>> So this is the right time for further testing of applications: >>>> Isabelle2018 should work as well, but I have

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
On 22/01/2019 23:08, Fabian Immler wrote: > On 1/22/2019 4:00 PM, Fabian Immler wrote: >> On 1/22/2019 2:28 PM, Makarius wrote: >>> On 22/01/2019 20:05, Fabian Immler wrote: >>>> These numbers look quite extreme: >>>> The slowdown in polyml-5.

Re: [isabelle-dev] State of the art in Isabelle with OCaml, opam and zarith

2019-01-22 Thread Makarius
time, somewhere in some dark corner. Apart from that, I've recently seen Coq experts worry about the status-quo of Opam: it is not as well-developed as Stack for Haskell, and Coq already critically depends on it. Makarius ___ isabelle-d

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
o some smaller parts of these sessions, where the effect is visible? We can then use profiling to get an idea what actually happens in x86_64_32. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
On 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HO

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
On 22/01/2019 12:31, Bertram Felgenhauer wrote: > Makarius wrote: >> So this is the right time for further testing of applications: >> Isabelle2018 should work as well, but I have not done any testing beyond >> "isabelle build -g main" -- Isabelle development only mo

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-22 Thread Makarius
On 19/01/2019 21:43, Makarius wrote: > Thanks to great work by David Matthews, there is now an Isabelle > component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be > enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this: > > init_component "$HO

[isabelle-dev] Poly/ML x86_64_32 available for testing

2019-01-19 Thread Makarius
mid-range hardware. There are additional memory requirements outside the ML heap, for program code and stacks. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Makarius
On 18/01/2019 21:55, Tobias Nipkow wrote: > Hey, I wanted to join the party! But all bugs have been fixed now and > Makarius will notify you of the correct changeset. Yes, see Isabelle/b18353d3fe1a. Despite the carnival season, I am presently working with David Matthews to make the canon

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Makarius
re is a natural routine of "hg commit" vs. "isabelle build -a" to make it all work well without any effort. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] mercurial accident

2019-01-18 Thread Makarius
ations, including our important model of having just one branch, i.e. no branches at all. With further branches, the situation would become much worse, like the average project on github. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum

Re: [isabelle-dev] mercurial accident

2019-01-17 Thread Makarius
On 17/01/2019 21:54, Makarius wrote: > > The problem behind this: Angeliki got administrative push-access to the > Isabelle repository, without anybody at Cambridge showing her how to use it. > > There is of course README_REPOSITORY, but the text is long. Here is the > u

Re: [isabelle-dev] mercurial accident

2019-01-17 Thread Makarius
e "hg view" (or equivalent) to ensure that the change is really what you want to make eternal when pushed to public. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Website https://isabelle.in.tum.de is down

2019-01-14 Thread Makarius
On 14/01/2019 18:47, Makarius wrote: > The website https://isabelle.in.tum.de appears to be down, this also > includes the Mercurial repository view at > https://isabelle.sketis.net/repos/isabelle > > Access via SSH works fine, thus the following clone is up-to-date within > an

[isabelle-dev] Website https://isabelle.in.tum.de is down

2019-01-14 Thread Makarius
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

2019-01-13 Thread Makarius
On 11/01/2019 11:51, Makarius wrote: > On 10/01/2019 16:38, Makarius wrote: >> On 10/01/2019 16:28, Florian Haftmann wrote: >>> Code generation: command 'export_code' without file keyword exports >>> code as regular theory export, which can be materialized using tool &g

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-01-11 Thread Makarius
On 10/01/2019 16:38, Makarius wrote: > On 10/01/2019 16:28, Florian Haftmann wrote: >> Code generation: command 'export_code' without file keyword exports >> code as regular theory export, which can be materialized using tool >> 'isabelle export'; to get generated code du

Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-01-10 Thread Makarius
to write it to the file-system via Generated_Files.write_files. * secondary output works via the Export interface to Isabelle/Scala; e.g. I could easily add Generated_Files.export_files for that and export_code would merely use Generated_Files.add_files (no

[isabelle-dev] NEWS: isabelle update

2019-01-06 Thread Makarius
y use double quotes for char/string literals, instead of slightly odd double single-quotes. Here is a reminder of the general approach and trend of recent years: * embedded languages normally use cartouches, while double quotes are old-style /

[isabelle-dev] Update of Haskell Stack

2018-12-28 Thread Makarius
ering. Thus "latest" things require more than one close look before adopting them. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

2018-12-27 Thread Makarius
ng HOL-Library.Cardinal_Notations (which > HOL-Cardinals.Cardinals does transitively). It would be great to see this all consolidated and somehow unified, i.e. some standard notation in Main as proposed by Larry (potentially as bundles as proposed by Florian), and avoidance of too much no_syntax rem

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-11-30 Thread Makarius
On 30/11/2018 21:56, Makarius wrote: > On 30/11/2018 19:45, Thomas Sewell wrote: > > I am also unsure why "archive formats" got on this thread. The heap is a > binary build artifact, with its own internal structure. Its precise > content is somewhat non-deterministic,

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-11-30 Thread Makarius
to refer persistently to physical file locations, or to build other non-portable information into the heap. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-11-30 Thread Makarius
tem is more complex and more easily destroyed by packaging it. These days I see big and complex products doing it our way: providing a fully integrated distribution for end-users that by-passes OS package managers. Makarius signature.asc Description: OpenPGP digital signature ___

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-11-30 Thread Makarius
On 30/11/2018 16:30, Jonathon Fernyhough wrote: > On 30/11/2018 14:55, Makarius wrote: >> On 30/11/2018 14:15, Jonathon Fernyhough wrote: >>> >>> I'm currently packaging Isabelle2018 (in deb format) for deployment to >>> several machines. These packages

Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts

2018-11-30 Thread Makarius
On 24/11/2018 19:51, Makarius wrote: > > *** Isabelle/jEdit Prover IDE *** > > * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle > DejaVu" collection by default, which provides uniform rendering quality > with the usual Isabelle symbols.

Re: [isabelle-dev] Support in `isabelle build` for SOURCE_DATE_EPOCH

2018-11-30 Thread Makarius
of it active. Also note that "isabelle build" uses SHA1 hash keys on the sources, not datestamps. Makarius signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Isabelle DejaVu fonts

2018-11-24 Thread Makarius
On 24/11/2018 19:51, Makarius wrote: > *** General *** > > * The font family "Isabelle DejaVu" is systematically derived from the > existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" > and styles "Norma

[isabelle-dev] NEWS: Isabelle DejaVu fonts

2018-11-24 Thread Makarius
v versions might have to revisit their Isabelle/jEdit properties, to ensure that no "IsabelleText" font specifications are left. Already existing user properties take precedence over defaults provided by Isabelle/jEdit: see $ISABELLE_HOME_USER/jedit/properties vs. $ISABELLE_HOME/src/Tools/jE

Re: [isabelle-dev] illegal reflective access

2018-11-17 Thread Makarius
On 15/11/2018 22:13, Makarius wrote: > On 15/11/2018 19:44, Lawrence Paulson wrote: >> Got this upon launch. Is it important? >> >> 341ebf35464b tip >> >> WARNING: Illegal reflective access by macosx.MacOSXPlugin to method >> com.apple.eawt.Ful

Re: [isabelle-dev] illegal reflective access

2018-11-15 Thread Makarius
to use fontforge to make a proper font instead. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

2018-11-11 Thread Makarius
uild process in user-space. It would also mean to get rid of the special "isabelle jedit -b" in various situations of system initialization. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS: Support for Isabelle command-line tools defined in Isabelle/Scala

2018-11-10 Thread Makarius
hich where interpreted. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
On 08/11/2018 21:32, Makarius wrote: > Over the decades we have accumulated funny quotation forms in Isabelle > syntax that are often hard to explain to new users (also to old users). I don't have a full overview of all the fine points yet, but the general idea is like this: * cart

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
E.g. one could set a date for the "big sweep" and make one big changeset, or one could gradually update entries in an erratic manner. You can probably say better if there are problems to be expected between the "stable" and "d

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
the document source in the text style of the term language At some point there will more Prover IDE support to add/remove the various formal comments (with control symbols and cartouches) that have emerged recently. But the old inner syntax is not

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-09 Thread Makarius
On 08/11/2018 21:36, Lawrence Paulson wrote: >> On 8 Nov 2018, at 20:32, Makarius wrote: >> >> In particular, what are the remaining uses of {* ... *}? > > I didn’t even know that existed. It was used a lot with the 'section' and 'text' commands until recently. Th

[isabelle-dev] Remaining uses of {* ... *} quotation?

2018-11-08 Thread Makarius
ot; to get rid of it (as well as `alt_string`). The long-term trend is to converge to cartouches or double-quotes almost everywhere. Cartouches are for nested languages, and double quotes for string literals or names that are in conflict with other syntax.

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
tack" and "opam" stack-up considerable material: it is easy to fill 5-15 GB of disk space after working some time. Only docker requires even more space. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.in

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
remove the "isabelle ghc" tool entry points: these auxiliary scripts should go into $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular Isabelle tools. I have now also learned that "ghci" is just "ghc --interactive", so there is no point to treat it too prominently.

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
On 08/11/2018 12:16, Makarius wrote: > On 08/11/2018 11:30, Bertram Felgenhauer wrote: >> Makarius wrote: >>> Nonetheless, it is still possible to use "isabelle ghc" without stack: >>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the >&g

Re: [isabelle-dev] NEWS: support for GHC

2018-11-08 Thread Makarius
On 08/11/2018 11:30, Bertram Felgenhauer wrote: > Makarius wrote: >> Nonetheless, it is still possible to use "isabelle ghc" without stack: >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the >> Isabelle settings mechanism to override ISABELLE_GH

[isabelle-dev] NEWS: Isabelle/PIDE modules for Haskell

2018-11-07 Thread Makarius
r me, even with friendly hints via hlint. Unfortunately I failed to reproduce the installation on my mobile machine. This reminds a bit of ancient times with vi and emacs, before Isabelle/PIDE/jEdit. Makarius ___ isabelle-dev mailing list isabelle-...

Re: [isabelle-dev] NEWS: support for GHC

2018-11-07 Thread Makarius
On 07/11/2018 16:32, Bertram Felgenhauer wrote: > Makarius wrote: >> *** System *** >> >> * Support for Glasgow Haskell Compiler via command-line tools "isabelle >> ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_st

Re: [isabelle-dev] jdk-11

2018-10-25 Thread Makarius
On 13/10/2018 22:39, Makarius wrote: >> >> I've quickly tried openjdk-11 on Ubuntu 18.10 beta: the same low-grade >> font rendering. It is particularly bad in Isabelle/jEdit file-open dialog. > > Thanks to a useful hint by the "Felix von Leitner Institute for >

  1   2   3   4   5   6   7   8   9   10   >