[isabelle-dev] ATP Vampire via internet / vampire for Mac

/sledgehammer.html Just use the attached script (named vampire) instead of the prover executable. Fabian Immler -- next part -- An embedded and charset-unspecified text was scrubbed... Name: vampire Url: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev

[isabelle-dev] NEWS

* Generic ATP manager for Sledgehammer, based on ML threads instead of Posix processes. Avoids potentially expensive forking of the ML process. New thread-based implementation also works on non-Unix platforms (Cygwin). Provers are no longer hardwired, but defined within the theory via plain ML

Re: [isabelle-dev] Grouping of Isabelle Symbols

this information more prominently (like in Symbols.bsh) On 11/21/2012 02:32 PM, Fabian Immler wrote: See also changeset 4ff5d795ed08, which introduces a dockable for symbols. As it is included in the repository, I guess it supersedes the macro in your collection -- I could have thought about porting

Re: [isabelle-dev] Announcing Isabelle work: Access Modifiers for Scala Code Generator

Hi Florian and Lukas, Am 04.05.2013 um 09:07 schrieb Florian Haftmann florian.haftm...@informatik.tu-muenchen.de I am curious to to see the already existing and emerging changes. Maybe there are already some things to point out then. The attached small patch is used in our setting: - every

Re: [isabelle-dev] Announcing Isabelle work: Access Modifiers for Scala Code Generator

Am 07.05.2013 um 09:59 schrieb Fabian Immler imm...@in.tum.de: For conceptual advances, there has also been the idea of providing a slot for pragmas for serializers: One use-case is the need to add pragmas for the target language in the generated code, but they could also be used to advise

Re: [isabelle-dev] isabelle root access

Markus Westerlind is a student of mine. For his Bachelor's thesis he needs to carry out performance measurements on a machine with many cores (isabelle-server). His project is not directly related to Isabelle, so you are right that a full root access is too much, but it is the only way for him

Re: [isabelle-dev] isabelle root access

Exactly the same applies to Yutaka. Fabian Am 10.07.2013 um 13:30 schrieb Makarius makar...@sketis.net: On Wed, 10 Jul 2013, Fabian Immler wrote: Markus Westerlind is a student of mine. For his Bachelor's thesis he needs to carry out performance measurements on a machine with many cores

Re: [isabelle-dev] Multicores at TUM

Am 10.07.2013 um 13:54 schrieb Makarius makar...@sketis.net: On Wed, 10 Jul 2013, Fabian Immler wrote: For his Bachelor's thesis he needs to carry out performance measurements on a machine with many cores (isabelle-server). What is this project anyway? It is about evaluating libraries

[isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)

Hi isabelle-dev, Makrius should know already, but I think it is a good idea to inform everyone here that a current student's project is about to provide a bit more advanced user interface for the find theorems functionality. It should be finished in two weeks time. Fabian

Re: [isabelle-dev] some actual find_theorems functionality (fb1f026c48ff)

Am 05.08.2013 um 18:02 schrieb Makarius makar...@sketis.net: On Sun, 4 Aug 2013, Fabian Immler wrote: I think it is a good idea to inform everyone here that a current student's project is about to provide a bit more advanced user interface for the find theorems functionality. It should

Re: [isabelle-dev] Ordinary_Differential_Equations FAILED

Hi, complete_univ has been renamed to complete_UNIV in Isabelle 1a13325269c2 (after the fork for the release). I therefore assume that I can commit the relevant changes to afp-devel. Best, Fabian Am 31.10.2013 um 10:53 schrieb Florian Haftmann florian.haftm...@informatik.tu-muenchen.de:

Re: [isabelle-dev] »real« considered harmful

I think I could live without real: coercions save a lot of the writing. Moreover, the real_of_foo abbreviations help to avoid type annotations: I suppose that all of the current occurrences of real could be replaced with one particular real_of_foo. For reading (subgoals etc), one could perhaps

[isabelle-dev] Non-responding Isabelle/jEdit and Monitor panel

Hi, I observed (in at least a99125aa964f) that when Isabelle/jEdit has been running for some time (about 2 to 4 hours perhaps), the GUI starts to "hang": every 3-4 seconds, the GUI does not respond to inputs for about half a second. I realized that this is apparently related to the Monitor

Re: [isabelle-dev] the function "real"

One example was broken and I fixed it in 06bfc5cfaeab, but the rest went through as usual. Fabian > Am 12.11.2015 um 11:00 schrieb Fabian Immler <imm...@in.tum.de>: > > Some examples have always been very slow. But I will double-check and mark > the slow ones as (*

Re: [isabelle-dev] NEWS: State panel

Hi Makarius, I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example: lemma assumes False shows "False ∧ False" (*using assms*) apply simp If you trigger output on the

Re: [isabelle-dev] The coming release of Isabelle2017

A while ago, Florian Haftmann sent a command that does something like this to the mailing list [1]. I attach a version that works with current Isabelle2016-1 (not sure if I got all the modifications right, but it seems to work at least on the example in the .thy file). Fabian [1]

Re: [isabelle-dev] Slow builds due to excessive heap images

> Am 03.11.2017 um 14:56 schrieb Fabian Immler <imm...@in.tum.de>: > > >> Am 02.11.2017 um 18:00 schrieb Makarius <makar...@sketis.net>: >> >> I am more worried about the factor 5 performance loss of Lorenz_C0: now >> (3:26:41 elapsed time, 1

Re: [isabelle-dev] Slow builds due to excessive heap images

692/x86_64-darwin: 522.080s elapsed time, 568.676s cpu time, 42.602s GC time > Am 03.11.2017 um 16:36 schrieb Fabian Immler <imm...@in.tum.de>: > > > >> Am 03.11.2017 um 14:56 schrieb Fabian Immler <imm...@in.tum.de>: >> >> >>> Am 02.11.2017 um 18

Re: [isabelle-dev] Slow builds due to excessive heap images

I should have sent the message below also to isabelle-dev, sorry about that. Has anything changed about integers in Poly/ML 5.7.1? Lorenz_C0 did slow down by a factor of 5, which I find quite extreme. Best, Fabian > Am 28.10.2017 um 23:57 schrieb Fabian Immler <imm...@in.tum.de>: >

Re: [isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

> Am 12.05.2018 um 00:27 schrieb Makarius : > > Isabelle/fad29d2a17a5 > parent: 68072:493b818e8e10 > parent: 68070:8dc792d440b9 > user:immler > date:Thu May 03 15:07:14 2018 +0200 > merged; resolved conflicts manually (esp. lemmas that have been

Re: [isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

> Am 14.05.2018 um 13:24 schrieb Fabian Immler <imm...@in.tum.de>: > > I did notice that those changes caused issues with timeouts in some AFP > sessions, and simply "fixed" those on the spot (e.g., the ones in afp/85324e3 > and afp/2ff575e hinted at problems

Re: [isabelle-dev] NEWS: isabelle jedit options

> Am 05.06.2018 um 23:01 schrieb Makarius : > > These options are very relevant for the coming release. I am interested > to get feedback from early adopters, if this is already sufficient or > requires further refinement. > > In other words, the question behind this: Can be get rid of most >

Re: [isabelle-dev] HOL-ODE-Numerics vs. HOL-ODE-Refinement

My impression is also that it is better to keep HOL-ODE-Numerics non-slow: Changes in HOL-Analysis often break HOL-ODE-Numerics, and I think it is better to get that feedback earlier (on Jenkins, isatest, or a private -a -X slow build) Fabian Am 31. Mai 2018 23:24:50 MESZ schrieb Makarius :

Re: [isabelle-dev] NEWS: sightly more parallel checking

> Am 05.06.2018 um 13:39 schrieb Makarius : > > On 04/06/18 20:17, Fabian Immler wrote: >> >> This "something in the background" appears to happen on a regular basis: >> every 2-3 seconds, the poly process consumes 200%CPU for about a se

Re: [isabelle-dev] NEWS: sightly more parallel checking

> Am 05.06.2018 um 14:47 schrieb Makarius : > > On 05/06/18 14:45, Fabian Immler wrote: >> >> >>>> The only way to stop this apparently is to invalidate something in the >>>> beginning of the (currently open) theory. >>> >&g

Re: [isabelle-dev] Gromov Hyperbolicity

> Am 18.01.2018 um 14:36 schrieb Tobias Nipkow <nip...@in.tum.de>: > > > > On 18/01/2018 11:06, Fabian Immler wrote: >>> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow <nip...@in.tum.de>: >>> >>> 1. Library/Complement contains both

Re: [isabelle-dev] Gromov Hyperbolicity

> Am 18.01.2018 um 08:32 schrieb Tobias Nipkow : > > 1. Library/Complement contains both new generic material like "t3_space" but > also new concepts like [mono_intros] for more automation in proving of > inequalities. In short, there is a wealth of material that might be

[isabelle-dev] Code check failed for SML on lxbroy10

Dear isabelle-dev, I noticed that currently (isabelle:ed0a7090167d, AFP:26f074817c9a) AFP/Native_Word fails to build on lxbroy10 (with ML_system_64=true): *** Code check failed for SML: isabelle process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure *** At command

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

or 'a^'n^'m, but I am not sure how well theorems can be transferred in that direction... Fabian > If there really is a common basis for formalising linear algebra than I would > be thrilled to see it, and I'm sure we could figure out a way to implement > this. > > Larry &

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

unifying the existing theories would be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do the construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec. Any opinions on that? Fabian > Larry > >> Begin forwarded message: >> >> From: Fabian Immler <i

[isabelle-dev] mercurial accident

The changesets a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7 seem to be the result of some mercurial/merge accident. They break HOL-Analysis, and it is not really clear from the history why and how to repair it. The last working version is 56acd449da41. Any opinions on what would be the best

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

On 1/22/2019 4:00 PM, Fabian Immler wrote: On 1/22/2019 2:28 PM, Makarius wrote: On 22/01/2019 20:05, Fabian Immler wrote: These numbers look quite extreme: The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as it seems to be the case with polyml-test-0a6ebca445fc

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

On 1/22/2019 2:28 PM, Makarius wrote: On 22/01/2019 20:05, Fabian Immler wrote: These numbers look quite extreme: The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as it seems to be the case with polyml-test-0a6ebca445fc). The following is isabelle/ab5a8a2519b0 afp

Re: [isabelle-dev] mercurial accident

Thanks for your feedback! I did what Lars suggested (96a43caa). Luckily, a diff with a8faf6f15 revealed quite obviously what went wrong during the merges, so I could easily redo Angeliki's tagging (689997a8). We should be back to normal (regarding isabelle build -a). Fabian On 1/17/2019

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

These numbers look quite extreme: The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as it seems to be the case with polyml-test-0a6ebca445fc). The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0: ML_PLATFORM="x86-linux" ML_OPTIONS="--minheap 2000 --maxheap

[isabelle-dev] syntax highlighting of inner comments

Hi, Up until Isabelle2018, I used (* ... *) to comment out parts of lemmas/definitions, mostly for debugging larger expressions. Highlighted in red, (* ... *) was nicely set apart from the rest of the expression. Now (e.g., isabelle/b58a575d211e) we can use \<^cancel>, but its

Re: [isabelle-dev] syntax highlighting of inner comments

gray ... Right now, when using Isabelle 2018, I do not use cancel, but (**), getting a warning, but having highlighting at least. Peter Original Message Subject: [isabelle-dev] syntax highlighting of inner comments From: Fabian Immler To: isabelle-dev@mailbroy.informatik.tu

Re: [isabelle-dev] Redundant definitions in Analysis

On 3/7/2019 7:36 AM, Lawrence Paulson wrote: In Analysis, we have two equivalent definitions of continuous functions between two topological spaces: lemma "continuous_map X Y f = continuous_on_topo X Y f" by (auto simp add: continuous_map_def continuous_on_topo_def vimage_def image_def

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

Great, thanks for looking into this! Fabian On 1/23/2019 4:24 PM, David Matthews wrote: On 23/01/2019 21:08, Makarius wrote: On 23/01/2019 12:05, David Matthews wrote: I've had a look at this under Windows and the problem seems to be with calls to IntInf.divMod from generated code, not from