Re: [isabelle-dev] Redundant definitions in Analysis

[Fabian Immler]

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 Collect_conj_eq inf_commute)

The first one comes from HOL Light and is defined in Abstract_Topology. The 
latter is declared in Function_Topology.

Obviously we need to eliminate one of them, and I prefer the former name. The 
latter is more logical but clunky, especially when compound with others in 
theorem names.
Sébastien might have a stronger opinion (I don't), but I would also go 
for continuous_map: it is in line with open_map, closed_map, 
quotient_map (which we don't have as constants, but use in theorem 
names). Moreover, we have more occurrences of continuous_map (174+0 vs 
83+39 in isabelle+AFP).


Fabian



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

Oh, you are right - there was a thread about that on isabelle-users in 
July/August/November, e.g.:

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-July/msg00124.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-August/msg00146.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-November/msg2.html

Fabian

On 3/6/2019 7:32 PM, Peter Lammich wrote:

Hi Fabian

I already pointed out the missing highlighting of cancel a few months 
ago ... I am still strongly in favor of having a highlighting that can 
easily be distinguished, eg the legacy red, or perhaps 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-muenchen.de
CC:


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
"highlighting" in black makes it very hard to keep an overview.

Note that e.g., with a type error in a lemma statement, canceled
text is
highlighted red (like in the attached screenshot).

Best regards,
Fabian

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] syntax highlighting of inner comments

[Fabian Immler]

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 
"highlighting" in black makes it very hard to keep an overview.


Note that e.g., with a type error in a lemma statement, canceled text is 
highlighted red (like in the attached screenshot).


Best regards,
Fabian


smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 IntInf.pow.  The
underlying RTS call used by IntInf.quotRem has changed in the 32-in-64
version.  It previously returned the pair of values by passing in a
stack location and having the RTS update this.  That isn't possible in
the 32-in-64 version so now it allocates a pair on the heap.  For
simplicity this is now used for the native code versions as well.  From
what I can tell nearly all the threads are waiting for mutexes and I
suspect that the extra heap allocation in IntInf.quotRem is causing some
of the problem.  Waiting for a contended mutex can cost a significant
amount of processor time both in busy-waiting and in kernel calls.

I'm not sure what to suggest except not to use concurrency here.  There
doesn't seem to be a way to avoid allocating a pair in IntInf.quotRem.


In the meantime David has produced Poly/ML a444f281ccec and I can
confirm that it works very well:


I had another look and it was a mutex contention problem, just not 
exactly where I'd thought.  Most calls to the run-time system involved 
taking a lock for a very short period in order to get the thread's C++ 
data structure.  This wasn't a problem in the vast majority of cases but 
this example involves very many calls to the long-format arbitrary 
precision package.  That resulted in contention on the lock.  I've 
changed this so the lock is no longer needed and it seems to have solved 
the problem.


David




smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

On 1/22/2019 4:00 PM, Fabian Immler wrote:

On 1/22/2019 2:28 PM, Makarius wrote:

On 22/01/2019 20:05, Fabian Immler wrote:

These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).

The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:

ML_PLATFORM="x86-linux"
ML_OPTIONS="--minheap 2000 --maxheap 4000"
Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time,
factor 2.66)
Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time,
factor 1.46) > (I am testing HOL-ODE-ARCH-COMP with
polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take 
some time...)
HOL-ODE-ARCH-COMP looked fine (2-3 times slower). But I realized that 
this was the case with your computations, too. Unlike Lorenz_C0:


> x86_64_32-linux -minheap 1500
> Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44)
> x86_64-linux --minheap 3000
> Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52)
Lorenz_C0 had the most significant slowdown, it has the biggest number 
of parallel computations, so I thought this might be related.


And indeed, if you try the theory at the end:
Par_List.map (with 6 cores, on Windows) is 12 times slower on _64_32 
whereas the sequential evaluation is only 2 times slower.


All of this reminds me of the discussion we had in November 2017:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2017-November/thread.html#7643

Fabian


==
theory Scratch
  imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin

definition "logistic p r x =
  normfloat (float_round_down p (float_round_down p (r * x)) * 
(float_plus_down p 1 (-x)))"


primrec iter where
  "iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"

definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1)) 
(nat_of_integer i)"


ML ‹val logistic_chaos = @{code logistic_chaos}›
ML ‹Par_List.map logistic_chaos (replicate 10 10)›
― ‹x86_64_32: 24s
   x86_64: 2s›
ML ‹map logistic_chaos (replicate 10 10)›
― ‹x86_64_32: 16s
   x86_64: 8s›

end



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

On 1/22/2019 2:28 PM, Makarius wrote:

On 22/01/2019 20:05, Fabian Immler wrote:

These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as
it seems to be the case with polyml-test-0a6ebca445fc).

The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:

ML_PLATFORM="x86-linux"
ML_OPTIONS="--minheap 2000 --maxheap 4000"
Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time,
factor 2.66)
Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time,
factor 1.46)


Can you point to some smaller parts of these sessions, where the effect
is visible? We can then use profiling to get an idea what actually
happens in x86_64_32.
It should be the by (tactic ...) invocations, which ultimately run 
generated code as an oracle (the one defined via @{computation_check} 
here: 
https://bitbucket.org/isa-afp/afp-devel/src/5d11846ac6abdad9c9dfee108d2772ac71c6179c/thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy#lines-2449)


The term that is being evaluated should be printed when declaring
[[ode_numerics_trace]].
(But it takes a lot of time to get there...)

I would have assumed that it is the heavy use of int computations that 
makes the difference, and it should be precisely the kind that is tested 
in the attached Float_Test.thy.


On my Windows-Laptop and on lxcisa0, however, I see the expected 
slowdown of about a factor of 2, but not more...


Could the issue be related to specific machines?
(I am testing HOL-ODE-ARCH-COMP with 
polyml-test-0a6ebca445fc/x86_64_32-linux right now, but that does take 
some time...)


Fabian


theory Float_Test
  imports
"HOL-Library.Float"
"HOL-Library.Code_Target_Numeral"
begin

definition "logistic p r x =
  normfloat (float_round_down p (float_round_down p (r * x)) * (float_plus_down 
p 1 (-x)))"

primrec iter where
  "iter p r x 0 = x"
| "iter p r x (Suc n) = iter p r (logistic p r x) n"

definition "logistic_chaos i = iter 30 (Float 15 (-4)) (Float 1 (-1)) 
(nat_of_integer i)"

ML \val logistic_chaos = @{code logistic_chaos}\
ML \logistic_chaos 100\

end

smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

These numbers look quite extreme:
The slowdown in polyml-5.7.1-8 is about a factor of 2-3 (and not 30 as 
it seems to be the case with polyml-test-0a6ebca445fc).


The following is isabelle/ab5a8a2519b0 afp/f49f0b0ead38 on lxcisa0:

ML_PLATFORM="x86-linux"
ML_OPTIONS="--minheap 2000 --maxheap 4000"
Finished HOL-ODE-Numerics (0:25:27 elapsed time, 1:07:49 cpu time, 
factor 2.66)
Finished HOL-ODE-ARCH-COMP (0:18:01 elapsed time, 0:26:19 cpu time, 
factor 1.46)



ML_PLATFORM="x86_64-linux"
ML_OPTIONS="--minheap 2000 --maxheap 4000"
Finished HOL-ODE-Numerics (0:29:34 elapsed time, 1:21:08 cpu time, 
factor 2.74)
Finished HOL-ODE-ARCH-COMP (0:06:49 elapsed time, 0:12:41 cpu time, 
factor 1.86)


Fabian

On 1/22/2019 11:36 AM, Makarius wrote:

On 19/01/2019 21:43, Makarius wrote:

Thanks to great work by David Matthews, there is now an Isabelle
component polyml-test-0a6ebca445fc (Isabelle/3b777286c3ec), which can be
enabled manually, e.g. in $ISABELLE_HOME_USER/etc/settings like this:

   init_component "$HOME/.isabelle/contrib/polyml-test-0a6ebca445fc"

It requires the usual "isabelle components -a" incantation afterwards.


polyml-test-0a6ebca445fc is the default in 81ca77cb7c8c, it means the
scope of further testing has widened.

Almost everything has become faster by default, but an exception are
heavy-duty int computations that rely on a certain word size, notably
the HOL-ODE family of sessions.

AFP/a04825886e71 marks various sessions explicitly as "large", which
means that they prefer x86_64.

Here are concrete numbers:

x86_64_32-linux -minheap 1500
Finished Pure (0:00:15 elapsed time, 0:00:15 cpu time, factor 1.00)
Finished HOL (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45)
Finished HOL-Analysis (0:03:48 elapsed time, 0:21:27 cpu time, factor 5.64)
Finished Ordinary_Differential_Equations (0:01:14 elapsed time, 0:05:31
cpu time, factor 4.43)
Finished Differential_Dynamic_Logic (0:01:29 elapsed time, 0:05:03 cpu
time, factor 3.39)
Finished HOL-ODE-Numerics (0:17:51 elapsed time, 0:46:30 cpu time,
factor 2.60)
Finished Lorenz_Approximation (0:04:02 elapsed time, 0:07:46 cpu time,
factor 1.92)
Finished Lorenz_C1 (0:00:04 elapsed time, 0:00:05 cpu time, factor 1.10)
Finished HOL-ODE-ARCH-COMP (0:12:56 elapsed time, 0:28:35 cpu time,
factor 2.21)
Finished HOL-ODE-Examples (0:37:13 elapsed time, 2:51:00 cpu time,
factor 4.59)
Finished Lorenz_C0 (3:46:03 elapsed time, 28:01:18 cpu time, factor 7.44)

x86_64-linux --minheap 3000
Finished Pure (0:00:16 elapsed time, 0:00:16 cpu time, factor 1.00)
Finished HOL (0:02:44 elapsed time, 0:09:28 cpu time, factor 3.47)
Finished HOL-Analysis (0:04:05 elapsed time, 0:22:47 cpu time, factor 5.58)
Finished Ordinary_Differential_Equations (0:01:19 elapsed time, 0:05:49
cpu time, factor 4.40)
Finished Differential_Dynamic_Logic (0:01:33 elapsed time, 0:05:22 cpu
time, factor 3.44)
Finished HOL-ODE-Numerics (0:18:59 elapsed time, 0:49:00 cpu time,
factor 2.58)
Finished Lorenz_Approximation (0:04:01 elapsed time, 0:07:39 cpu time,
factor 1.90)
Finished Lorenz_C1 (0:00:03 elapsed time, 0:00:03 cpu time, factor 1.20)
Finished HOL-ODE-ARCH-COMP (0:04:06 elapsed time, 0:08:37 cpu time,
factor 2.10)
Finished HOL-ODE-Examples (0:05:18 elapsed time, 0:17:04 cpu time,
factor 3.22)
Finished Lorenz_C0 (0:06:52 elapsed time, 0:51:44 cpu time, factor 7.52)


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] mercurial accident

[Fabian Immler]

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 3:54 PM, Makarius wrote:

On 17/01/2019 21:42, Lars Hupel wrote:

Strip the accidental changes from the repository?


Never strip public changesets.


Indeed. "Fixing" a desaster by non-monotonic operations is a desaster
squared.





Back out the changes?


You can't really back out merges, as far as I know.


Or do a no-op merge from a successor of the last working version?


This is also not possible, I think.

Do this instead:

$ hg revert -a -r 56acd449da41
$ hg commit -m "revert to 56acd449da41"


This looks fine and obvious.


The problem behind this: Angeliki got administrative push-access to the
Isabelle repository, without anybody at Cambridge showing her how to use it.

There is of course README_REPOSITORY, but the text is long. Here is the
ultra-short version:

   After every local commit, use "hg view" (or equivalent) to ensure that
the change is really what you want to make eternal when pushed to public.


Makarius





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] mercurial accident

[Fabian Immler]

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 way to continue from here?

Strip the accidental changes from the repository?
Back out the changes?
Or do a no-op merge from a successor of the last working version?

Fabian



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> Am 05.06.2018 um 23:01 schrieb Makarius :
> 
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.
> 
> In other words, the question behind this: Can be get rid of most
> auxiliary images in AFP (e.g. "Foo_Lib", "Pre_Foo")?
I started to use -S HOL-ODE-Numerics and got rid of HOL-ODE-Refinement (which 
was such an auxiliary image) in AFP/cf739ca.
-S is very helpful because it reduces the start-up time for Isabelle/jEdit 
(with the AFP in ROOTS) from 100s to 30s (compared to -R).

I can also imagine that auxiliary images get outdated easily (importing too 
much or too little), and so it is good that -R/-S takes care of this potential 
maintenance efforts.

Fabian

smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> 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.
>>> 
>>> It should be possible to achieve this effect by removing the concluding
>>> 'end' command.
>> Just now I was in the middle of a theory (without any 'end' command), where 
>> every (are they supposed to happen periodically?) "consolidation" took about 
>> 4 seconds.
>> 
>> It seems like something is accumulating somewhere when editing the document, 
>> because after invalidating the beginning of the theory and going back to the 
>> same place as before, the "consolidation" was not noticeable any more.
> 
> What kind of theory is this? Many commands? Long-running /
> non-terminating commands?
In this particular case, it was a relatively short theory (300 lines) with no 
long-running or non-terminating commands. I inserted and removed some 
diagnostic commands (code_thms, export_code foo in SML), but those were not 
present anymore when I observed this 4-second-consolidation-loop.

Fabian

smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> 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 second.
>> poly should be idle (or used to be in such a situation) because (as far
>> as I can tell) nothing else (e.g., sledgehammer, find theorems) seems to
>> be active.
> 
> This is probably due to the implicit "consolidation" of finished
> theories, which I have made a bit more official as PIDE document edit
> (see Isabelle/09ac56914b29). That is important, because of the final
> "presentation", e.g. for generated LaTeX.
> 
> In Isabelle/38272f9481c2, I have also changed the delay from 1s to 2.5s
> -- you can make this 10s or more until I figure out a way to reduce the
> impact of it.
Thanks, this really seems to be the "consolidation": I can see the effect of 
chainging editor_consolidate_delay.

>> The only way to stop this apparently is to invalidate something in the
>> beginning of the (currently open) theory.
> 
> It should be possible to achieve this effect by removing the concluding
> 'end' command.
Just now I was in the middle of a theory (without any 'end' command), where 
every (are they supposed to happen periodically?) "consolidation" took about 4 
seconds.

It seems like something is accumulating somewhere when editing the document, 
because after invalidating the beginning of the theory and going back to the 
same place as before, the "consolidation" was not noticeable any more.

Fabian




smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 :
>On 31/05/18 16:36, Makarius wrote:
>> 
>> Anyway, with approx. 100min CPU time HOL-ODE-Numerics has become
>> eligible for the "AFP slow" category: paradoxically this will make
>the
>> test much faster, but also less accurate in its timing information,
>> because the test hardware and settings are quite different.
>
>Several sessions depend on HOL-ODE-Numerics:
>HOL-ODE-Examples, Lorenz_Approximation, Lorenz_C0, Lorenz_C1
>
>So it is better to keep it as non-slow: otherwise the whole tower needs
>to be moved.
>
>
>   Makarius
>___
>isabelle-dev mailing list
>isabelle-...@in.tum.de
>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> 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 caused by incorporating syntax for FuncSet 
> into Complex_Main).
> This was just to keep everything going, but I was well aware that I needed to 
> take a closer look at the problems caused there and resolve them properly 
> (e.g., not exposing FuncSet-syntax in Complex_Main).
I did move FuncSet back to HOL-Library in isabelle/2af1f142f855 and 
afp/5d961e9f8536.
It seems like this improved the performance a lot:

isabelle/2af1f142f855
afp/5d961e9f8536
-
Finished JinjaThreads (0:35:12 elapsed time, 2:28:07 cpu time, factor 4.21)
0:35:24 elapsed time, 2:28:07 cpu time, factor 4.18

Before it was:
isabelle/48262e3a2bde
afp/7dde4e79f45a
-
Finished JinjaThreads (0:54:35 elapsed time, 3:32:25 cpu time, factor 3.89)
0:58:01 elapsed time, 3:43:03 cpu time, factor 3.84

We will have to wait for the results on
https://isabelle.sketis.net/devel/build_status/AFP_slow_64bit_6_threads/index.html#session_JinjaThreads
to see whether this is actually back to normal or whether there are more 
performance problems.

In JinjaThreads/Common/ExternalCall.thy one can see that e.g., in definition 
red_external_aggr, the funcset syntax → causes
"Ambiguous input⌂ produces 32768 parse trees" and therefore takes 6 minutes 
(instead of 1 second).

Fabian




smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> 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 moved
> from Linear_Algebra and Cartesian_Euclidean_Space)
> 
> 
> That merge is a total mess -- as a consequence of disregarding long
> established customs from README_REPOSITORY:
It is a mess, indeed. But it is "almost" a trivial merge: the conflicts with 
the other branch isabelle/0a2a1b6507c1
to isabelle/8dc792d440b9 are mostly cosmetic changes, local to proofs.

Now I think that it might have been over-ambitious to get all of these 
developments into the repository in just two steps (afp/5bbb50b with 
isabelle/0a2a1b6507c1 and then the move to isabelle/493b818e8e10).
For the sake of a cleaner history, it might have been worth re-doing those 
changes in smaller steps, but I could not spend an arbitrary amount of time on 
this project.
Now the changesets do at least reflect the actual history (it did take me two 
weeks to complete the parent 493b818e8e10).
And I did not want to keep those changes in private drawers for much longer.
These changesets are actually the result of reviving (and completing) work that 
Johannes (Hölzl) started in November 2017. Given this long time span, 
everything actually worked out reasonably well.

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 caused by incorporating syntax for FuncSet 
into Complex_Main).
This was just to keep everything going, but I was well aware that I needed to 
take a closer look at the problems caused there and resolve them properly 
(e.g., not exposing FuncSet-syntax in Complex_Main).

It is great that we have this detailed history of performance measurements, 
otherwise I would not have dared to push changes that caused timeouts in some 
of the sessions, not knowing about degrading performance in others...
Makarius, thanks a lot for maintaining this infrastructure and also keeping an 
eye on the performance figures!

> Maybe he can sort that out.

I was planning to investigate this in the course of this week.

Fabian



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> Am 26.02.2018 um 16:12 schrieb Lawrence Paulson <l...@cam.ac.uk>:
> 
> I was at the meeting in Logroño and my impression was that we had to live 
> with these different formalisations. There was no way to unify them and the 
> best one could hope to transfer certain results from one formalisation to 
> another using local types in some incredibly complicated way.
HMA_Connect shows a way to unify (at least parts of) them: it makes explicit 
that 'a^'n^'m can be seen as a subtype of 'a mat.

This makes it possible to avoid duplications: for example, results about 
eigenvalues are only proved once for 'a mat and are transferred to the 
"subtype" 'a^'n^'m.
In contrast to that, we do have duplicate developments for determinants, 
multiplication etc. in isabelle and the AFP. We should be able to get rid of 
those.

Ideally, one would do the developments for '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
> 
>> On 26 Feb 2018, at 14:57, Fabian Immler <imm...@in.tum.de 
>> <mailto:imm...@in.tum.de>> wrote:
>> 
>> We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
>> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and 
>> that there are formalizations of (aspects of) linear algebra for both of 
>> them. Last year in Logrono, there was the proposal to put all linear algebra 
>> on the common foundation of a locale for modules, but apparently nobody has 
>> found the time and motivation to push this much further.
>> 
>> Perhaps a more humble first step towards 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?
> 



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> Am 26.02.2018 um 12:54 schrieb Lawrence Paulson <l...@cam.ac.uk>:
> 
> Is there a case for moving some material from this file into the Analysis 
> directory?
> 
> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
> 
> Many of the results proved at the end of this file are quite straightforward 
> anyway. As somebody with a lifting-and-transfer phobia, I don't feel 
> qualified to make this decision. Possibly these techniques are overkill. I 
> have already proved some of these results quite straightforwardly using 
> linearity, and installed them not long ago.
For the record, "not long ago" is c8caefb20564. I generalized this to the same 
class constraints as in HMA_Connect in d97a28a006f9.

Yes, I guess these techniques are overkill for the (straightforward) proofs of
matrix_add_vect_distrib,
matrix_vector_right_distrib,
matrix_vector_right_distrib_diff,
matrix_diff_vect_distrib
(they are exactly the lemmas touched by d97a28a006f9). I left them in 
HMA_Connect.thy as examples for the transfer_hma method.

The remaining lemmas at the end of HMA_Connect are probably not so easy to move 
to the distribution: they involve concepts that are missing in HOL-Analysis, 
e.g., eigen_value, charpoly, or similar_matrix.

We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
Analysis/Finite_Cartesian_Product both formalize vectors and matrices and that 
there are formalizations of (aspects of) linear algebra for both of them. Last 
year in Logrono, there was the proposal to put all linear algebra on the common 
foundation of a locale for modules, but apparently nobody has found the time 
and motivation to push this much further.

Perhaps a more humble first step towards 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 <imm...@in.tum.de>
>> Subject: Re: [isabelle] Matrix-Vector operation
>> Date: 26 February 2018 at 08:02:40 GMT
>> To: isabelle-users <isabelle-us...@cl.cam.ac.uk>
>> Cc: Omar Jasim <oajas...@sheffield.ac.uk>
>> 
>> Dear Omar,
>> 
>> Unfortunately, there are no lemmas on distributivity of *v in the 
>> distribution.
>> Some are currently in the AFP-entry Perron_Frobenius:
>> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
>> 
>> You can prove them (in HOL-Analysis) as follows:
>> 
>> lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: 
>> ring_1 ^ 'n)"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum_subtractf left_diff_distrib)
>> 
>> lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum.distrib distrib_right)
>> 
>> lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum.distrib distrib_left)
>> 
>> lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v 
>> (v - w) = M *v v - M *v w"
>>  unfolding matrix_vector_mult_def
>>  by vector (simp add: sum_subtractf right_diff_distrib)
>> 
>> Those should probably be included in the next Isabelle release.
>> 
>> Hope this helps,
>> Fabian
>> 
>> 
>>> Am 25.02.2018 um 19:27 schrieb Omar Jasim <oajas...@sheffield.ac.uk>:
>>> 
>>> Hi,
>>> 
>>> This may be trivial but I have a difficulty proving the following lemma:
>>> 
>>> lemma
>>> fixes  A :: "real^3^3"
>>>   and x::"real^3"
>>> assumes "A>0"
>>> shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "
>>> 
>>> where A is a positive definite diagonal matrix. Is there a lemma predefined
>>> related to this?
>>> 
>>> Cheers
>>> Omar
>> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 "export_code" (line 889 of 
"~/work/afp/afp-devel/thys/Native_Word/Bits_Integer.thy")

The build works fine on e.g., lxbroy8. It also works on lxbroy10 with 
ML_system_64=false.

This is apparently since the introduction of polyml-5.7.1 
(isabelle:aefaaef29c58, AFP:c7180aa1cb8f).

Stripping the problem down, I realized that this has nothing to do with 
Native_Word, because the same issue arises with the following theory:

theory Test imports HOL.Code_Generator begin
export_code Code_Generator.holds checking SML
end

The log says:

Loading theory "Test.Test"
/home/immler/.isabelle/contrib/jdk-8u162/x86_64-linux/jre/bin/java: symbol 
lookup error: /usr/lib64/libhogweed.so.4: undefined symbol: __gmpn_cnd_add_n
### theory "Test.Test"
### 0.291s elapsed time, 0.009s cpu time, 0.000s GC time
*** Code check failed for SML: isabelle process -e 'datatype ref = datatype 
Unsynchronized.ref' -f 'ROOT.ML' -l Pure
*** At command "export_code" (line 5 of "/mnt/home/immler/Test.thy")

Does anyone have an idea about this?
There seems to be an issue with the libraries on lxbroy10, but I wonder why 
this is only triggered with "export_code ... checking SML".

Best regards,
Fabian





smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Fabian Immler]

> 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 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 
>>> suitable for inclusion in HOL-Analysis.
>>> I have already made a start by moving a few [simp] rules but that is it 
>>> from me because I am not familiar enough with the Analysis material.
>> Most of this looks like it could go to HOL-Analysis.
>>> 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of 
>>> generic concepts that should go somewhere else.
>>> We need a discussion on whether any of the theories deserve a separate AFP 
>>> entry.
>> In my opinion, Hausdorff_Distance and Metric_Completion are general enough 
>> to put them to HOL-Analysis.
>> (They are also relatively short, so I am not sure if it is worth to create 
>> separate AFP entries.)
>> The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, 
>> and quasi-isometries.
>> The very same definition of Lipschitz maps is also in 
>> AFP/Ordinary_Differential_Equations, so I take this as a strong indication 
>> to move Lipschitz maps to HOL-Analysis. Isometries also seem like a 
>> generically useful concept and could go to HOL-Analysis.
> 
> A lot of things are useful, but Isometries.thy is large and would also make a 
> nice AFP entry.
With "Isometries" I meant the part of Isometries.thy that introduces 
isometry_on (this is only 150 lines). Lipschitz maps are another 350 lines.
The rest of Isometries.thy seems to be about geodesic spaces and 
quasi-isometries could indeed make a separate AFP entry.

Fabian

>> My impression is that geodesic spaces and quasi-isometries are more 
>> specialised concepts (but that might also be just because I have never come 
>> across them up to now...). I have no real opinion on what to do with them.
>> We do not have a precise specification of what HOL-Analysis is or should be. 
>> I think that makes it very hard to draw a line between material that should 
>> go to HOL-Analysis and what should remain in the AFP. So take this as just 
>> my personal view.
>> Fabian
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Fabian Immler]

> 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 suitable 
> for inclusion in HOL-Analysis.
> I have already made a start by moving a few [simp] rules but that is it from 
> me because I am not familiar enough with the Analysis material.
Most of this looks like it could go to HOL-Analysis.

> 2. Hausdorff_Dinstance, Metric_Completion and Isometries stronly smell of 
> generic concepts that should go somewhere else.
> We need a discussion on whether any of the theories deserve a separate AFP 
> entry.
In my opinion, Hausdorff_Distance and Metric_Completion are general enough to 
put them to HOL-Analysis.
(They are also relatively short, so I am not sure if it is worth to create 
separate AFP entries.)

The theory Isometries contains Lipschitz maps, isometries, geodesic spaces, and 
quasi-isometries.
The very same definition of Lipschitz maps is also in 
AFP/Ordinary_Differential_Equations, so I take this as a strong indication to 
move Lipschitz maps to HOL-Analysis. Isometries also seem like a generically 
useful concept and could go to HOL-Analysis.

My impression is that geodesic spaces and quasi-isometries are more specialised 
concepts (but that might also be just because I have never come across them up 
to now...). I have no real opinion on what to do with them.


We do not have a precise specification of what HOL-Analysis is or should be. I 
think that makes it very hard to draw a line between material that should go to 
HOL-Analysis and what should remain in the AFP. So take this as just my 
personal view.

Fabian



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

I looked at it once more: profiling told me that IntInf.pow (in combination 
with Par_List.map) seems to be the culprit.

The following snippet shows similar behavior:
ML ‹
fun powers [] = []
 | powers (x::xs) = IntInf.pow (2, x mod 15)::powers xs;
Par_List.map (fn i => powers (i upto 10 * i)) (0 upto 31)
›

polyml-5.6-1/x86_64-linux: 0:00:08 elapsed time, 0:00:35 cpu time, factor 4.02
polyml-test-e8d82343b692/x86_64-linux: 0:00:36 elapsed time, 0:03:26 cpu time, 
factor 5.70
polyml-5.6-1/x86_64-darwin:  0.570s elapsed time, 1.748s cpu time, 0.000s GC 
time
polyml-test-e8d82343b692/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: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, 16:49:16 cpu time, factor 4.88). It is unclear if
>>> the problem is related to Flyspeck-Tame. I did not approach it yet,
>>> because the HOL-ODE tower is really huge.
>>> 
>>> It would greatly help to see the problem in isolated spots. I usually
>>> send David specimens produced by code_runtime_trace.
>> At least on my Mac, there seems to be a problem with (or induced by) 
>> parallelism:
>> The attached check.sml is the code extracted from Lorenz_C0.
>> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in 
>> the computation for individual elements.
>> 
>> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, 
>> something goes very wrong: a slowdown by a factor of more than 50, compared 
>> to Isabelle2017 .
>> 
>> This seems to be related to parallelism:
>> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. 
>> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.
>> 
>> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this 
>> behaves for both parallel and sequential computations like Isabelle2017.
>> 
>> Unfortunately, I failed to reproduce this behavior on Linux.
> 
> I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
> 1600 --maxheap 4000" if that is relevant).
> Invoked with "isabelle build -d . -othreads=8" for the theory below.
> 
> polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu 
> time, factor 6.94)
> polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 
> 4.70)
> 
> Both are in isabelle/123670d1cff3
> 
> --
> 
> theory Check
> imports Pure
> begin
> 
> ML_file \check.sml\
> ML \timeap Check.check (0 upto 7)\
> 
> end
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

> 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, 16:49:16 cpu time, factor 4.88). It is unclear if
>> the problem is related to Flyspeck-Tame. I did not approach it yet,
>> because the HOL-ODE tower is really huge.
>> 
>> It would greatly help to see the problem in isolated spots. I usually
>> send David specimens produced by code_runtime_trace.
> At least on my Mac, there seems to be a problem with (or induced by) 
> parallelism:
> The attached check.sml is the code extracted from Lorenz_C0.
> "Check.check xs" does a Par_List.forall on the list xs and Par_list.map in 
> the computation for individual elements.
> 
> With isabelle/fc87d3becd69 and polyml-test-e8d82343b692/x86_64-darwin, 
> something goes very wrong: a slowdown by a factor of more than 50, compared 
> to Isabelle2017 .
> 
> This seems to be related to parallelism:
> In check_seq.sml, I replaced Par_List.forall/Par_list.map with list_all/map. 
> In this case isabelle/fc87d3becd69 behaves more or less like Isabelle2017.
> 
> I also tried isabelle/fc87d3becd69 with polyml-5.6-1/x86_64-darwin: this 
> behaves for both parallel and sequential computations like Isabelle2017.
> 
> Unfortunately, I failed to reproduce this behavior on Linux.

I think I could reproduce the problem on lxcisa0 (with ML_OPTIONS="--minheap 
1600 --maxheap 4000" if that is relevant).
Invoked with "isabelle build -d . -othreads=8" for the theory below.

polyml-test-e8d82343b692/x86_64-linux: (0:02:37 elapsed time, 0:18:11 cpu time, 
factor 6.94)
polyml-5.6-1/x86_64-linux: (0:00:30 elapsed time, 0:02:24 cpu time, factor 4.70)

Both are in isabelle/123670d1cff3

--

theory Check
imports Pure
begin

ML_file \check.sml\
ML \timeap Check.check (0 upto 7)\

end




smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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>:
> 
> Lorenz_C0 is one of those "much slower" sessions.
> If it helps, this is how I would characterize it:
> It is essentially one long computation where the code (IIRC about 15000 lines 
> in SML) was generated in the parent session Lorenz_Approximation via 
> @{computation_check ...}). The computation depends heavily on IntInf 
> operations (but mostly in the <64 bit range)
> 
> Fabian
> 
>> Am 28.10.2017 um 22:45 schrieb Makarius <makar...@sketis.net>:
>> 
>> On 28/10/17 22:26, Makarius wrote:
>>> We are presently testing Poly/ML 5.7.1 by default (see
>>> Isabelle/aefaaef29c58) and there are already interesting performance
>>> figures, e.g. see:
>>> 
>>> http://isabelle.in.tum.de/devel/build_status
>>> http://isabelle.in.tum.de/devel/build_status/Linux_A
>>> http://isabelle.in.tum.de/devel/build_status/AFP
>> 
>> The daily "AFP slow" timing has arrived just now, 4h hours later than
>> with Poly/ML 5.6:
>> http://isabelle.in.tum.de/devel/build_status/AFP_slow_64bit_6_threads
>> 
>> I still need to investigate, why some sessions require much longer now.
>> It might be due massive amounts of generated code.
>> 
>> 
>>  Makarius
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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] 
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04443.html



Explorer.thy
Description: Binary data

> Am 09.07.2017 um 16:58 schrieb Lawrence Paulson :
> 
> What I’m requesting requires no sophistication at all. It is merely to 
> automate what we currently do by copying from one window and pasting to 
> another, while inserting “fix”, “assume” and “show” in the obvious places.
> Larry
> 
>> On 9 Jul 2017, at 16:32, Lars Hupel  wrote:
>> 
>> I currently supervise a student who's investigating proof refactoring. One 
>> possible outcome of this would be a tool that also does what you suggested. 
>> It's a little too early to tell, though.
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 (* slow *) to reduce confusion in the future.
> 
> Fabian
> 
>> Am 11.11.2015 um 18:29 schrieb Johannes Hölzl <hoe...@in.tum.de>:
>> 
>> Okay, I look at the AFP entries.
>> 
>> I assume Affine_Arithmetic is just slow, but I can ask Fabian tomorrow
>> if this is unusual.
>> 
>> - Johannes
>> 
>> Am Mittwoch, den 11.11.2015, 17:19 + schrieb Lawrence Paulson:
>>> It would be great if you could help. I have just committed some
>>> corrections to a number of AFP theories, including that one I think.
>>> Affine_Arithmetic comes with some examples that run extremely slowly;
>>> I’m not sure whether there is a problem or whether it is always like
>>> that. If you want to take over with those, I can do some more tidying
>>> up with the main libraries.
>>> 
>>> Larry
>>> 
>>>> On 11 Nov 2015, at 17:17, Johannes Hölzl <hoe...@in.tum.de> wrote:
>>>> 
>>>> Hi Larry,
>>>> 
>>>> this is a huge change and after I adapted Markov_Models I see that it
>>>> simplifies some proofs.
>>>> 
>>>> If you want I can adapt all AFP entries for which I'm the maintainer, or
>>>> which are related to Probability theory:
>>>> 
>>>> Density_Compiler
>>>> Integration
>>>> Lower_Semicontinuous
>>>> Markov_Models
>>>> Ordinary_Differential_Equations
>>>> Possibilistic_Noninterference
>>>> Probabilistic_Noninterference
>>>> UpDown_Scheme
>>>> Girth_Chromatic
>>>> Probabilistic_System_Zoo
>>>> Random_Graph_Subgraph_Threshold
>>>> pGCL
>>>> 
>>>> Just tell me which of these you are already working on, so we can merge
>>>> without conflicts.
>>>> 
>>>> - Johannes
>>>> 
>>>> 
>>>> Am Mittwoch, den 11.11.2015, 12:28 + schrieb Lawrence Paulson:
>>>>> I’m glad to have your support. It’s just possible that I might ask your 
>>>>> help in getting some things working in the AFP.
>>>>> 
>>>>> Larry
>>>>> 
>>>>>> On 10 Nov 2015, at 17:53, Manuel Eberl <ebe...@in.tum.de> wrote:
>>>>>> 
>>>>>> This is very nice to hear. ‘real’ has plagued me for some time now and I 
>>>>>> am glad to see it gone.
>>>>>> 
>>>>>> Thanks for the good work!
>>>>>> 
>>>>>> 
>>>>>> On 10/11/15 17:45, Lawrence Paulson wrote:
>>>>>>> The first phase of this project is finished: the function “real” now 
>>>>>>> has the monomorphic type nat => real and is simply an abbreviation for 
>>>>>>> the generic function, of_nat. In addition, the function “real_of_int” 
>>>>>>> abbreviates the generic function of_int.
>>>>>>> 
>>>>>>> It took about a week to convert all the theories in the main 
>>>>>>> Isabelle/HOL directory. Most of them needed little or no attention, the 
>>>>>>> big exceptions being Probability (which frequently used “real” with the 
>>>>>>> type ereal => real) and Decision_Procs, which contained many thousands 
>>>>>>> of instances of “real” on integers and floats.
>>>>>>> 
>>>>>>> The main priority at the moment is to fix the decision procedure mir, 
>>>>>>> which isn’t working but appears to be entirely unused. Then there is 
>>>>>>> still a lot of cleaning up to do, especially in Real.thy and its 
>>>>>>> ancestors. Two or three dozen theorems existed in duplicate forms, with 
>>>>>>> versions for “real” separate from versions for the other coercions; 
>>>>>>> occasionally these variants were named systematically, but often their 
>>>>>>> names were unrelated from the originals, and the names of variables in 
>>>>>>> the theorems were almost always different. The simplification status of 
>>>>>>> the two variants generally differed as well. Thus the behaviour of the 
>>>>>>> simplifier on a formula depended on which coercion had been used, and 
>>>>>>> in 150 cases, the simplification itself included the mapping of one 
>>>>>>> coercion to another (there were two equivalent theorems for doing this).
>>>>>>> 
>>>>>>> Innumerable type constraints have now become redundant (things such as 
>>>>>>> real_of_int (i::int)), but I intend to leave them as they are. I have a 
>>>>>>> lot of AFP entries to fix.
>>>>>>> 
>>>>>>> Larry
>>>> 
>>>> 
>>>> ___
>>>> isabelle-dev mailing list
>>>> isabelle-...@in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>> 
>> 
>> 
>> ___
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 panel: clicking 
"Reset" there resolves the problem.

Best regards,
Fabian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: State panel

[Fabian Immler]

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 "apply simp" command, you get 1 subgoal in the 
State panel.
Now uncomment "using assms" and trigger output again (on the "apply simp" 
command): the State panel does not change.

I just noticed that this behavior only occurs when the output is triggered with 
a keyboard shortcut, clicking on the "Update" button yields the expected 
behavior.

Having worked with the "new" interaction model for half a day, I am wondering 
if it could make sense to trigger output in the State panel also implicitly 
with cursor movements?
That would require less explicit interaction with the IDE but still save 
(some?) resources (if I am guessing correctly that previously all intermediate 
proof states have been pretty printed and rendered in the background while now 
it would only happen on demand).

Best regards,
Fabian


> Am 09.11.2015 um 21:41 schrieb Makarius :
> 
> * The State panel manages explicit proof state output, with jEdit action
> "isabelle.update-state" (shortcut S+ENTER) to trigger update according
> to cursor position.
> 
> * The Output panel no longer shows proof state output by default. This
> reduces resource requirements of prover time and GUI space.
> INCOMPATIBILITY, use the State panel instead or enable option
> "editor_output_state".
> 
> 
> This refers to Isabelle/bb20f11dd842.  The State panel has been around for a 
> while, without mentioning it explicitly.  It should now be sufficiently 
> consolidated for production use; even old GUI timing problems that caused 
> excessive flashing due to repaints should no longer happen.
> 
> Disabling option editor_output_state allows to get back to the traditional 
> Isabelle/jEdit behaviour, but tradtionalists might actually like the new 
> State panel better, because it is closer to Proof General (in the newer 
> 3-buffer model, not the truely traditional 2-buffer model).
> 
> 
>   Makarius
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 think about less obstructive 
abbreviations like e.g., real_N and real_Z, or real⇩N and real⇩Z.
But I see that real_of_foo is much more uniform and you can immediately read 
off the type foo.

Fabian

 Am 03.06.2015 um 10:11 schrieb Tobias Nipkow nip...@in.tum.de:
 
 For me the main point of real is the ease of writing. If we get rid of some 
 lemma duplications but trade that in for many type annotations, I am not in 
 favour.
 
 Tobias
 
 On 02/06/2015 20:18, Florian Haftmann wrote:
 Dear all,
 
 recently, I stumbled (once again) over the matter of the »real« conversion.
 
 There is an inclusion hierarchy (⊆) of numerical types
 
  (num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex
 
 We can embed »smaller« into »bigger« types using conversions
 
  (numeral ⊆) of_nat ⊆ of_int ⊆ of_rat ⊆ of_real
 
 These conversions have solid generic algebraic definitions!
 
 For historic reasons, there is also the conversion real :: 'a ⇒ real
 which is overloaded and can be instantiated to arbitrary types. This
 (co)conversion works in the other direction without any algebraic
 foundation!
 
 My impression is that having this conversion is a bad idea. For
 illustration have a look at
 http://isabelle.in.tum.de/repos/isabelle/file/3d696ccb7fa6/src/HOL/Archimedean_Field.thy#l312
 which gives a wonderful generic lemma relating fraction division and
 integer division:
 
  »floor (of_int k / of_int l) = k div l«
 
 Note that the result type of the of_int conversion is polymorphic and
 can be instantiated to rat and real likewise!
 
 In the presence of the »real« conversion, there is a second variant
 
  »floor (real k / real l) = k div l«
 
 which must be given separately!
 
 For uniformity it would be much better to have »real« disappear in the
 middle run. I see two potential inconveniences at the moment:
 * Writing »of_foo« might demand a type annotation on its result in many
 cases (n.b. operations of type foo ⇒ 'a are one of the rare cases where
 explicit type annotations must be given in terms rather than at »fixes«).
 * We have the existing abbreviations »real_of_foo« which have no type
 ambiguity, but might seem a little bit verbose.
 Anyway, the duplication seems more grivious to me than such syntax issues.
 
 Any comments?
  Florian
 
 
 
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
 
 
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Ordinary_Differential_Equations FAILED

[Fabian Immler]

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:

 Ordinary_Differential_Equations FAILED
 (see also 
 /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/Ordinary_Differential_Equations)
 
 sr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb/usr/share/texmf
 -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb/usr/share/texmf-dist/fonts/ty
 pe1/public/amsfonts/cm/cmmi7.pfb/usr/share/texmf-dist/fonts/type1/public/amsf
 onts/cm/cmmi8.pfb/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.p
 fb/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb/usr/share/
 texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb/usr/share/texmf-dist/font
 s/type1/public/amsfonts/cm/cmr7.pfb/usr/share/texmf-dist/fonts/type1/public/a
 msfonts/cm/cmr8.pfb/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmssi
 10.pfb/usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb/usr/s
 hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb/usr/share/texmf-dist
 /fonts/type1/public/amsfonts/cm/cmsy7.pfb/usr/share/texmf-dist/fonts/type1/pu
 blic/amsfonts/cm/cmti10.pfb/usr/share/texmf-dist/fonts/type1/public/amsfonts/
 symbols/msbm10.pfb
 Output written on root.pdf (97 pages, 436697 bytes).
 Transcript written on root.log.
 
 *** Unknown fact complete_univ (line 449 of 
 /mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy)
 *** At command using (line 448 of 
 /mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy)
 *** Unknown fact complete_univ (line 384 of 
 /mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy)
 *** At command using (line 384 of 
 /mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy)
 
 This refers to Isabelle 6d0688ce4ee2 and AFP 2a0f81020af9
 
 Any ideas?
 
   Florian
 
 -- 
 
 PGP available:
 http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
 
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 be finished in two weeks time.
 
 So far I only know about the existence of the project, but nothing about its 
 contents.
Well, it is supposed to provide a GUI for find_theorems, it should provide 
completion in the input, but also e.g. filtering of the output.
I currently cannot access the development, so I am afraid I cannot say anything 
more specific at the moment.

Fabian

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] isabelle root access

[Fabian Immler]

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 to access that 
machine (conveniently).
So he has nothing to do with Isabelle development or administration and I trust 
that he is not abusing his power.

Fabian



Am 10.07.2013 um 13:04 schrieb Makarius makar...@sketis.net:

 The Lehrstuhl at TUM has this ancient tradition to hand out full root 
 access (via the isabelle Unix group) to anybody who happens to get an 
 account for any kind of project.
 
 This is a lot of power (and responsibility) and and recent years we had quite 
 often the situation that neither the one who grants the rights nor the one 
 who receives them knows what that implies.
 
 So can anybody clarify the role of the new Isabelle administrator westerli 
 (Markus Westerlind)?
 
 Of course he is also welcome to introduce himself.
 
 
   Makarius
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] isabelle root access

[Fabian Immler]

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 
 (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 to access that machine (conveniently).
 
 So he has nothing to do with Isabelle development or administration and I 
 trust that he is not abusing his power.
 
 OK, that is what we've usually had routinely in the past.  BTW, these shadow 
 administrators don't even know their powers, so abuse has de-facto not 
 happened yet, as far as I know.  (This is a strange security policy, of 
 course.)
 
 Can you also speak for nagashim (Yutaka Nagashima)?
 
 
   Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Multicores at TUM

[Fabian Immler]

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 for parallelism in Haskell, in Markus' case 
Repa [1].
Yutaka uses Isabelle to generate code for another library, DPH [2].
There have been disappointing measurements, but they were mostly due to the 
fact that both libraries are still under development.

Fabian

[1] http://repa.ouroborus.net/
[2] http://www.haskell.org/haskellwiki/GHC/Data_Parallel_Haskell

 
 Note that isabelle-server has many cores (24), but the hardware structure is 
 made for many independent processes (e.g. virtual machines), not applications 
 that use shared-memory multithreading. Thus the results of measurement might 
 be a bit disappointing, depending on the kind of application.
 
 Intel Xeons (especially after Nehalem from 2009) are usually much better; 
 macbroy2 is the classic machine for that, although it is getting a bit old 
 now; I have the follow-up model in my office since 2010.  It is possible to 
 get a real warp factor of 9.6 for parallel Isabelle in the best situation (8 
 cores with hyperthreading).
 
 I have seen a really hot 16-core Xeon at TUM recently, but it seems to belong 
 to a different Lehrstuhl that is subject to the same system administration. 
  It runs some boring batch process with 16 threads since a couple of 
 weeks/months.
 
 
   Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 a serializer to export 
 only specific constants -- and these pragmas could be generated e.g. by the 
 export_code statement.

Another use case for pragmas would be the option to add (or modify) the (at the 
moment) hard-coded import statements, as proposed in [1].

Best,
Fabian

[1] http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/6887


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Fabian Immler]

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 target language has so-called interface functions, which are the ones 
to be exported (i.e. with a public modifier) by the target language.

So instead of
  export_code List.sublists in Scala
you would have to write something like
  code_interfaces Scala List.sublists
  export_code List.sublists in Scala

There are several shortcomings that should be addressed for applications in 
more general settings:
- the serializer should check wether the interface functions are actually 
used in the module
- usually, one probably wants the functions that are exported to be the ones 
that were declared in the export_code statement

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 a serializer to export 
only specific constants -- and these pragmas could be generated e.g. by the 
export_code statement.

Cheers,
Fabian



interfaces
Description: Binary data
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Grouping of Isabelle Symbols

[Fabian Immler]

2012/11/21 Christian Sternagel c-ste...@jaist.ac.jp:
 Hi again,

 I also think that the Encoding and Abbreviation TextAreas of my
 Symbols.bsh macro would be nice to have in your dockable.
At the moment (e2c08f20d00e) both of them are shown as tooltips on the buttons.
I might place 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 it
 to Scala, the current implementation is, however, relatively
 straightforward (and more dense compared to the Java code).

 If you have any comments or suggestions concerning the Symbols
 dockable, feel free
 to contact me!

 Regards,
 Fabian


 2012/11/21 Christian Sternagel c-ste...@jaist.ac.jp:

 Is there a plan to make the grouping of changeset 0226d408058b available
 in
 Isabelle/Scala through isabelle.Symbol? I could make use of it in the
 Symbols.bsh macro of

https://isabelle.in.tum.de/community/Extending_Isabelle/jEdit

 cheers

 chris

 PS: Is it possible to somehow use Scala when writing jEdit macros?
 Anyone?
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de

 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] NEWS

[Fabian Immler]

* 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 wrapper functions.

Basic sledgehammer commands:

- 'sledgehammer prover_1 ... prover_n' invokes the specified automated 
theorem provers on the first subgoal. Provers are run in parallel, the 
first successful result is displayed, and the other attempts are 
terminated. Provers are defined in the theory context, see also 
'print_atps'.

If no provers are given as arguments to sledgehammer, the system refers 
to the default defined as ATP provers preference by the user 
interface. There are additional preferences for timeout (default: 60 
seconds), and the maximum number of independent prover processes 
(default: 5); excessive provers are automatically terminated.

- 'print_atps' prints the list of automated theorem provers available to 
the sledgehammer command.

- 'atp_info' prints information about presently running provers

- 'atp_kill' terminates all presently running provers.

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

[Fabian Immler]

Dear all,

in the context of my work as student assistant, the following (for some 
of you perhaps useful) perl-script was developed:

It can be used if you cannot install Vampire(for the 
sledgehammer-tool)on your machine for instance if you use a Mac.

The script queries a proof-server 
(http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP) to solve problems 
and passes the solutions to isabelle.

Isabelle can use this script the same way it uses a locally installed 
Vampire.

So installation is similar to the installation of the 'real' vampire as 
described here: http://isabelle.in.tum.de/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/attachments/20080813/d9d6d87f/attachment.diff