Re: [isabelle-dev] Irrefutable patterns in Haskell and Quickcheck/Narrowing
Hi Florian, I have been quite busy the last few days and hence did find the time to answer you email quickly. > This however breaks Quickcheck/Narrowing where the lazy nature of > pattern bindings has been exploited, may be unconsciously. A minimal > example is attached (Quickcheck_Narrowing_Examples.thy) but I also > distilled the generated Haskell code: Quickcheck Narrowing inherently uses Haskell's lazy evaluation to have a evaluation engine that implements narrowing without actually transforming the program that is evaluated. The real ideas how to implement narrowing in Haskell come from the original authors of LazySmallCheck; the main contribution to make this possible in Isabelle is largely the engineering question how to combine the ideas from LazySmallCheck with the Isabelle code generator. As I was investigating this, I did some further extensions to allow existential quantifiers, but this is technically not that difficult to implement. There is a bit of documentation describing the implementation in my thesis. At the moment, I am a little bit busy, but hopefully mid of February, I could assist looking into this. Maintaining Quickcheck Narrowing has not been a major tasks in the last years there was no need to change anything as tricky as the point that we encounter now. Hence, I would expect that maintenance will continue to be low, once we resolved this issue. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: HOL-Spec_Check -- a Quickcheck tool for Isabelle's ML environment
* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment. With HOL-Spec_Check, ML developers can check specifications with the ML function check_property. The specifications must be of the form "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in src/HOL/Spec_Check/Examples.thy. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 05/30/2013 05:32 PM, Makarius wrote:
On Thu, 30 May 2013, Lukas Bulwahn wrote:
I was thinking of a ML antiquotation for "check_property @{context}"
and I was thinking of @{spec ...} and some context flags that lets
spec either only compile, or check with values.
This should allow that @{spec ...} could be inlined in the
implementation if anyone wishes to do so.
Do you know how to define the ML antiquotation, or shall I do it?
Please go ahead and do it when you have time.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 05/30/2013 03:51 PM, Makarius wrote:
So back to this now:
* Canonical session name? It looks like the name of the tool is
"Spec_Check", according to its main Spec_Check.thy
So it would be session HOL-Spec_Check in ~~/src/HOL/Spec_Check/
You still have a chance to rename "Spec_Check" now, before
anything is
pushed to main Isabelle. The directory location is given by having a
session built on HOL, though.
Yes, I think Spec_Check is the name to go with.
* Formal licensing. As part of the main source tree it implicitly
joins the toplevel LICENSE. It is possible to have a 1-line
add-on in
each theory header, e.g. see ~~/src/HOL/SPARK/SPARK.thy, but not a
separate LICENSE file.
There is no need for a separate LICENSE file here.
The README could also say in plain words that the original code-base
by Christopher League has been relicensed under the 3-clause BSD
license of Isabelle -- i.e. a slightly reduced version of what is in
the README of f0a79be57a4b already.
Yes, I was trying to point this out, but did not state it in such
precise words.
* NEWS and CONTRIBUTORS entries.
Summary and Authors are in the README file from that NEWS and
CONTRIBUTORS can be derived.
Further (less important hints on the README):
3. As Isabelle can run heavily in parallel, we avoid reference types.
Sounds like someone got surprised after 10 years of multicores in the
consumer market that parallel programming is just the normal
situation. When I was a young student, we did learn parallel and
concurrent programming by default, instead of the oo-nonsense that
came on later generations. (Times have changed again already, so we
don't have to revisit this old topic.)
4. Isabelle has special naming conventions and documentation of source
code is only minimal to avoid parroting.
Sounds a bit depressing for me, since I've tried to explain the good
old high-quality code writing techniques in the implementation manual,
and then the young people don't even fit sources on the screen (much
more than the 80--100 char line length). BTW, I've seen really good
sources recently: ACL2. They have a *strict* 80 char limit, and
really good writing style of "essays", not "code documentation".
Anyway, we stick to what Isabelle/ML is, and don't have to make
excuses for it.
These are no excuses, but they simply describe the reasons for the
differences between the original QCheck and the Isabelle's Spec_Check
implementation.
Dou you want to have a toplevel Isar command for "check_property
@{context}"? That is relatively easy to have these days. What should
be its name?
I was thinking of a ML antiquotation for "check_property @{context}"
and I was thinking of @{spec ...} and some context flags that lets spec
either only compile, or check with values.
This should allow that @{spec ...} could be inlined in the
implementation if anyone wishes to do so.
All of this is possible future work, but more importantly, I would like
to see some volunteer that advertises and mentors a follow-up student
project for Spec_Check.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
Hi everyone,
motivated by the current discussion, I used the Bavarian holiday today
to get the aforementioned Quickcheck tool into a stable state.
The latest stable version is at:
https://bitbucket.org/nicolai490/qcheck_tum
I will only have some spare time if at all to maintain it.
I hope someone at TUM is willing to take this over and
mentor a bachelor or master student, who could write
formal specifications for the unification and/or pattern
matching in Isabelle.
I bet quickchecking the specifications with appropriate
generators will uncover more surprises of the current
implementations.
@Makarius: Are you willing to include the current state in
Isabelle's repository, e.g. under src/Tools/?
The sources are in a stable state and maintenance in last
half year boiled down to only one minor change. Hence, I
believe that it is a low-maintenance part in Isabelle and can
be easily maintained the next few years with almost no
further effort.
Lukas
On 05/30/2013 12:23 AM, Tobias Nipkow wrote:
this incident has again reminded me that in the absence of formal proofs about
the code, assertions in the code would be a big step forward. they could have
told us a long time ago that some precondition expected by the unification code
is not guaranteed. lukas and a student had even put together a quickcheck
infrastructure for Isabelle/ML. All of this could be confined to regression
runs. i think we should make some effort in this direction to increase our
confidence in the kernel.
tobias
Am 27/05/2013 19:54, schrieb Makarius:
On Mon, 27 May 2013, Makarius wrote:
The change ensures that variables with equal name are unified, in the same
manner as the types of Free or Const are unified, before doing the real work
of HO-unification.
Here is another example for Isabelle/Pure, without schematic variables with
different types. It may be be tried before/after my change 3b9c31867707 from
today:
ML {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}
declare [[show_types]]
typedecl nat
typedecl bool
ML {*
val read = Syntax.read_term (Proof_Context.set_mode
Proof_Context.mode_schematic @{context});
val a = read "a :: nat => bool";
val x = read "?x :: ?'b";
*}
ML {* Seq.list_of (Unify.hounifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
ML {* Seq.list_of (Unify.unifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
ML {* Pattern.unify @{theory} (a, x) (Envir.empty 15); *}
Before the change, Unify.hounifiers crashes; after the change it is able to work
out the type instantiation correctly. Pattern.unify is still not quite there,
neither before nor after the change.
Note that the original implementation by Larry did try to unify the result types
in any case, using the body_type function. But that was assuming that the arity
of the function type happens to coincide with the number of arguments in the
term application.
This is why I introduced optional bounds to the function type traversal in
envir.ML 7f3549a316f4. Note that in 3b9c31867707 the type unification of the
disagreement pair is done explicitly via unify_types_of, without taking the
functions apart, but also see the modification of assignment where these bounds
correspond to the number of actual arguments.
For the moment, I am not going to produce more changes. Maybe Larry and Tobias
also want to comment, as the authors of these modules from some decades ago.
Stefan is of course the proven expert who re-investigated quite a lot of that
around 2000.
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
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
On 12/11/2012 10:27 PM, Makarius wrote: On Mon, 10 Dec 2012, Makarius wrote: On Fri, 30 Nov 2012, Lukas Bulwahn wrote: It must be considered unmaintained. The benchmarks themself I will irregularly have time on weekends and nights to have a look, but I cannot keep up with "Isabelle roaring ahead". After several weeks of isatest failing on HOL-Quickcheck_Benchmark (now at least reliably with Interrupt, not Timeout), the situation is still unchanged in the repository (presently 0a740d127187). In Isabelle/d466ebc27810 isatest is silenced for now, to give Lukas a window of opportunity to make up his mind. Note that src/HOL/ROOT has other quickcheck tests commented out for a long time already. If nothing happens, lets say until the last week of the year, I will start moving find_unused_assms to HOL/ex. Things have changed in 768a3fbe4149 and it solved the issue in find_unused_assms. Just for your information, it was due to a non-terminating code equation for the vimage constant. The Codegenerator_Test session only checks if code is generated but not if the executable equations make much sense, the find_unused_assm theory complements that by actually executing a number of generated programs and should not be dropped in the future if it ever breaks again. A failure in this theory indicates some open issue in the code generation process or setup. If other problems occur, I am willing to help whenever I can. However as I left Garching, it takes some time to address those issues. Makarius, thanks for your patience and your work bisecting the cause of the failure. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
On 12/11/2012 10:27 PM, Makarius wrote: On Mon, 10 Dec 2012, Makarius wrote: On Fri, 30 Nov 2012, Lukas Bulwahn wrote: It must be considered unmaintained. The benchmarks themself I will irregularly have time on weekends and nights to have a look, but I cannot keep up with "Isabelle roaring ahead". After several weeks of isatest failing on HOL-Quickcheck_Benchmark (now at least reliably with Interrupt, not Timeout), the situation is still unchanged in the repository (presently 0a740d127187). In Isabelle/d466ebc27810 isatest is silenced for now, to give Lukas a window of opportunity to make up his mind. Note that src/HOL/ROOT has other quickcheck tests commented out for a long time already. If nothing happens, lets say until the last week of the year, I will start moving find_unused_assms to HOL/ex. Things have changed in 768a3fbe4149 and it solved the issue in find_unused_assms. Just for your information, it was due to a non-terminating code equation for the vimage constant. The Codegenerator_Test session only checks if code is generated but not if the executable equations make much sense, the find_unused_assm theory complements that by actually executing a number of generated programs and should not be dropped in the future if it ever breaks again. A failure in this theory indicates some open issue in the code generation process or setup. If other problems occur, I am willing to help whenever I can. However as I left Garching, it takes some time to address those issues. Makarius, thanks for your patience and your work bisecting the cause of the failure. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Quickcheck_Benchmark timeouts
On 11/29/2012 06:27 PM, Makarius wrote: On Mon, 26 Nov 2012, Makarius wrote: In the past few weeks, we've had isatest problems with HOL-Quickcheck_Benchmark and ISABELLE_FULL_TEST=true (as used with mac-poly64-M4 and mac-poly64-M8). After some experimentation and tinkering, it seems that the timeouts in Isabelle/978200ae8473 from last Friday work: we've had successful isatest runs over the weekend. As far as I can see, the tests on macbroy2 terminate around 05:30 CET. This might be relavant for later tests of AFP. That was too optimistic. It seems that find_unused_assms uses a lot of stack space, and thus fills up memory on x86_64. I've addressed this in f25bcb8a4591 to get more explicit failure. I've also started some bisection about where the problem comes from, without any clear results so far, but I will report more a bit later. Is Lukas Bulwahn still looking after his stuff, or is this now unmaintained? It must be considered unmaintained. The benchmarks themself I will irregularly have time on weekends and nights to have a look, but I cannot keep up with "Isabelle roaring ahead". Lukas 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] HOL-Quickcheck_Benchmark timeouts
On 11/29/2012 10:22 PM, Makarius wrote:
On Thu, 29 Nov 2012, Makarius wrote:
I've also started some bisection about where the problem comes from,
without any clear results so far, but I will report more a bit later.
I've spent a few more hours on the problem, repeating the bisection
several times, and staring add various changesets that are not at all
clear from their text.
This is the result:
50e457bbc5fe bulwahn GOOD
6a26fed71755 bulwahn SKIP (BAD)
28cd3c9ca278 bulwahn SKIP (BAD)
fb696ff1f086 bulwahn BAD
Due to skipped revisions, the first bad revision could be any of:
changeset: 49943:6a26fed71755
user:bulwahn
date:Sat Oct 20 09:09:32 2012 +0200
summary: passing names and types of all bounds around in the simproc
changeset: 49944:28cd3c9ca278
user:bulwahn
date:Sat Oct 20 09:09:33 2012 +0200
summary: tuned tactic in set_comprehension_pointfree simproc to
handle composition of negation and vimage
changeset: 49945:fb696ff1f086
user:bulwahn
date:Sat Oct 20 09:09:34 2012 +0200
summary: adjusting proofs
And here some explanation reconstructed from the investigations with
some guesswork, glossing over the the unexplained things in these
changesets.
(1) BAD means the following crash:
theory A imports Main
begin
find_unused_assms Fun
Warning - Unable to increase stack - interrupting thread
Exception trace for exception - Interrupt
Generated_Code.value(1)(1)(1)(1)(2)
Generated_Code.check_all_subsets(4)(1)
Exhaustive_Generators.compile_generator_expr(2)compile-(1)(1)(1)(1)(1)
Exhaustive_Generators.compile_generator_expr(2)(1)(1)
Quickcheck_Common.test_term_with_cardinality(5)test_card_size(4)
Quickcheck_Common.test_term_with_cardinality(5)test(2)
Quickcheck_Common.test_term_with_cardinality(5)
Quickcheck_Common.generator_test_goal_terms(5)
(2) SKIP means these changesets were broken: HOL did not compile.
Backporting the "adjusting proofs" changeset fb696ff1f086, revealed
that they were BAD, too.
Note that it does not make any sense to publish changesets where Pure
or HOL do not compile. There is no obligation to have all session OK
all the time before pushing, but the usefulness of changesets is
greatly diminished. Someone else needs to spend much more time in
exchange for the 2-3 minutes saved in not running HOL on the spot,
before saying "hg commit". (I usually do a full "isabelle build -a"
before *any* commit.) And of course, there is an obligation to run
full "isabelle build -a" (or a proven equivalent) before any push.
(3) Looking at the critical change 6a26fed71755 "passing names and
types of all bounds around in the simproc" several times, I tried to
understand why it affects the generated quickcheck code in such a bad
way. (The changelog merely repeats the diff in English prose as a
"parrot".)
So after backing-out this single-line change from 5a1194acbecd of
today, everything worked fine except for
src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy crashing as follows:
*** Wellsortedness error
*** (in code equation Set_Comprehension_Pointfree_Tests.union ?a ?b ==
{x. x : ?a | x : ?b}):
*** Type nat not of sort enum
*** No type arity nat :: enum
*** At command "export_code" (line 134 of
"~~/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy")
Looking in the vicinity of the many other changes related to the
critical three above reveals the following:
changeset: 49947:29cd291bfea6
user:bulwahn
date:Sat Oct 20 09:09:37 2012 +0200
files: src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
description:
adding another test case for the set_comprehension_simproc to the
theory in HOL/ex
So here one could guess from the greater context that 6a26fed71755
with its SKIP (BAD) status was motivated by a problem with passing
sort information down to the generated code. Since this is the
"exhaustive" quickcheck tester, having "nat :: enum" or not could make
a difference in the amount of enumeration done here.
So "BAD" might actually mean "better" in the sense of more exhaustive,
but it breaks down the concrete application of find_unused_assms
nonetheless.
Another side remark: Isabelle does not have a tradition for "test
cases" and "unit tests". What we usually made in all these decades
were some half-decent applications to explore tools or some stylized
examples to show the main points. These then also serve as a tests
somehow. (There is sometimes the odd situation that some manual or
"test" theory is the only spot where certain features of certain tools
occur, which means there is lack of proof for practical relevance.
I've seen this again just today in a different situation that is
unrelated to this incident.)
Anyway, maybe Lukas himself or codegen export Florian knows how to
resolve the situation.
I could have time on the weekend to have a closer look again.
The time when these changesets were pushed was rather bad, as at that
time you were on
Re: [isabelle-dev] Warning "Simplifier: renamed bound variable" (was "set_comprehension_pointfree" simproc losing bounds
On 10/22/2012 08:22 AM, Lukas Bulwahn wrote: On 10/19/2012 04:35 PM, Makarius wrote: On Fri, 19 Oct 2012, Lukas Bulwahn wrote: Operations like Simplifier.context, Simplifier.inherit_context should help here. Once that is repaired, I will see if the warning can now be made an error that is more explicit about the reasons. I am certainly in favour of this. First, tool developers mainly react on errors with test runs, but do not see the warnings. Secondly, users do not know who to report those warnings and do not know if they are caused by their scripts or the tools. Historically, the weak warning was a necessity due to too many simprocs still not working with the context. Let's hope that it can be easily switched to an explicit error after so many years now. On the weekend, I had a look at this issue in the set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and already noticed what could make things difficult turning this into an error. Two examples: - the hypsubst_tac internally uses the simplifier, but the interface does not allow to pass the current simpset to this tactic. - An implementer has to avoid certain functions, such asRaw_Simplifier.rewrite, that assume to be used only in a non-nested context. I had a further look at the issue with the "Simplifier: renamed bound variable" to repair the set_comprehension_pointfree simproc and to turn the warning into an error for the future. However, I was very surprised that the warning occurs even if I pass around the context following typical Isabelle programming idioms. To state my expectation more formally: For every simpset ss and ss', I would expect Simplifier.context (Simplifier.the_context ss) ss' == Simplifier.inherit_context ss ss' Attached, there is an simple example that shows a warning for "Simplifier.context (Simplifier.the_context ss)", but it does not for Simplifier.inherit_context ss. Looking at the code of the simplifier, I did understand my misunderstanding: It is NOT ONLY "working with the context" correctly, but also "passing around the simpset" correctly---a programming paradigm that I (and probably many others) are not aware of. Lukas Scratch.thy Description: application/isabelle-theory ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP: Session AVL-Trees broken
On 11/07/2012 10:41 PM, Gerwin Klein wrote: On 08/11/2012, at 8:26 AM, Florian Haftmann wrote: Am 07.11.2012 22:22, schrieb Gerwin Klein: If I run sessions manually, they work fine, but they fail in the cron job with timeout (even small ones like Separation_Algebra). In the case of AVL-Trees, it fails interactively (i.e. fails in the stricter sense), at proofs seeming inherently difficult. There are bound to be some real errors in the noise after some time.. On this one we got: Building Refine_Monadic ... *** Timeout (but manages to finish the larger JinjaThreads) AVL-Trees FAILED (see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.0_x86-darwin/log/AVL-Trees) [..] *** Bad certificate cache: missing certificate *** At command "by" (line 169 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/AVL-Trees/AVL.thy") (real error) I can see no reason why any of these would have to time out, and they don't on other machines (I've only tried some, though, not all). Could it be an artefact of time measurement on macbroy 2 or something like that? Too many jobs in parallel? It doesn't seem to be very deterministic either, there are different sessions failing at different times. I can confirm that the AVL-Tree certification errors are real and the timeouts occur nondeterministically even on my laptop, when running "afp_build -A". Other than that, I am not aware of any other errors in the AFP. By the way, I cannot use mira on lxbroy1 to test the current tip, as mira does not update the repository for some strange reason. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] priority queues
I think priority queues are roughly ordered lists (the priority is the ordering). So, you could have a look at Pure/General/ord_list.ML Lukas On 10/24/2012 05:21 PM, Steffen Juilf Smolka wrote: Hi, is there an implementation of priority queues in the isabelle library? Steffen ___ 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] "set_comprehension_pointfree" simproc losing bounds
On 10/19/2012 04:35 PM, Makarius wrote: On Fri, 19 Oct 2012, Lukas Bulwahn wrote: Operations like Simplifier.context, Simplifier.inherit_context should help here. Once that is repaired, I will see if the warning can now be made an error that is more explicit about the reasons. I am certainly in favour of this. First, tool developers mainly react on errors with test runs, but do not see the warnings. Secondly, users do not know who to report those warnings and do not know if they are caused by their scripts or the tools. Historically, the weak warning was a necessity due to too many simprocs still not working with the context. Let's hope that it can be easily switched to an explicit error after so many years now. On the weekend, I had a look at this issue in the set_comprehension_pointfree simproc (cf. changeset 6250121bfffb) and already noticed what could make things difficult turning this into an error. Two examples: - the hypsubst_tac internally uses the simplifier, but the interface does not allow to pass the current simpset to this tactic. - An implementer has to avoid certain functions, such asRaw_Simplifier.rewrite, that assume to be used only in a non-nested context. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] the testboard is working unstable
On 10/19/2012 04:23 PM, Tjark Weber wrote: Hi Lukas, On Tue, 2012-10-16 at 18:23 +0200, Lukas Bulwahn wrote: the testboard was repeatedly breaking down today---and I restarted it multiple times to keep the illusion of a stable environment. I will investigate tomorrow what is going wrong. Until then, I'll try my best restarting it after a break-down as fast as possible. I tried using the testboard (for the first time actually) by pushing some changesets, and I am not sure they actually got tested: the three status indicator circles are gray, and there is no "running" indicator. Is this the expected behavior? I was not successful on Wednesday with my investigations and delegated it to Lars on Thursday and Friday. At the point of your push, the testboard did not run correctly. I don't know what happened on the weekend and who touched the subject, but it apparently works again today. Let's hope for the best that it works the next time you push some changes. You did everything correctly, and usually you would see green or red lights indicates success or failure, respectively. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "set_comprehension_pointfree" simproc losing bounds
On 10/19/2012 02:22 PM, Makarius wrote:
On Wed, 17 Oct 2012, Lukas Bulwahn wrote:
If you update to changeset 89b118c0c070, the issue should be resolved.
There still seem to be remaining issues: Isabelle/d1ecb3554b25 and
AFP/15527cc14202:
Girth_Chromatic FAILED
(see also
/Volumes/Macintosh_HD/Users/makarius/.isabelle/heaps/polyml-5.5.0_x86-darwin/log/Girth_Chromatic)
### Simplifier: renamed bound variable ":000" to ":000a" (line 588 of
"/Volumes/Macintosh_HD/Users/makarius/isabelle/afp-devel/thys/Girth_Chromatic/Girth_Chromatic.thy")
...
*** Tactic failed
*** The error(s) above occurred for the goal statement:
*** {(a, b). a : :000 & b : :000 & a < b} =
*** {(a, b) |a b. a : :000 & b : :000 & a < b}
*** (line 168 of
"/Volumes/Macintosh_HD/Users/makarius/isabelle/afp-devel/thys/Girth_Chromatic/Ugraphs.thy")
I was aware that there are still a couple of open issues, caused by the
newly introduced simproc.
At the moment, I am still hunting errors in the Isabelle repository, but
soon the errors in the AFP will be next.
The final crash is one thing, the long list of the above warnings
another. The warning means that the context for a nested simplifier
invocation is not right. Operations like Simplifier.context,
Simplifier.inherit_context should help here. Once that is repaired, I
will see if the warning can now be made an error that is more explicit
about the reasons.
I am certainly in favour of this. First, tool developers mainly react on
errors with test runs, but do not see the warnings. Secondly, users do
not know who to report those warnings and do not know if they are caused
by their scripts or the tools.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "set_comprehension_pointfree" simproc losing bounds
Hi Dmitriy,
If you update to changeset 89b118c0c070, the issue should be resolved.
Lukas
On 10/16/2012 01:41 PM, Dmitriy Traytel wrote:
Hi all,
the following produces a "Loose bound variable" with
Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma "finite {y |y. ∃x. y ∈ f x}"
apply simp
oops
end
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continue working on whatever
follows in the theory until this issue is fixed.
Best wishes,
Dmitriy
___
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] the testboard is working unstable
Hi all, the testboard was repeatedly breaking down today---and I restarted it multiple times to keep the illusion of a stable environment. I will investigate tomorrow what is going wrong. Until then, I'll try my best restarting it after a break-down as fast as possible. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?
Hi Florian, in the changeset e8400e31528a of the Isabelle repository, you moved the theorem Pair_inject in the Product_Type theory into a section called "Legacy theorem bindings and duplicates". In my current development, I rely on the theorem Pair_inject, and it is the most suitable rule for my purpose. Why was it considered legacy or a duplicate? Does this still hold at the current tip? NB: At the current tip d7917ec16288, I cannot find any duplicate theorem for Pair_inject. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "set_comprehension_pointfree" simproc losing bounds
Hi Dmitriy,
thanks for the report. I am working on this procedure currently, so this
will be fixed in a few changesets.
Lukas
On 10/16/2012 01:41 PM, Dmitriy Traytel wrote:
Hi all,
the following produces a "Loose bound variable" with
Isabelle/4a15873c4ec9
theory Scratch
imports Main
begin
lemma "finite {y |y. ∃x. y ∈ f x}"
apply simp
oops
end
Fortunately, jedit treats a proof that used to work (but fails now due
to the above) as a sorry, such that I can continue working on whatever
follows in the theory until this issue is fixed.
Best wishes,
Dmitriy
___
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] Editing HOL theories interactively
Hi Florian, just for the record: - I added those FIXMEs while adding the "set_comprehension_pointfree" simproc. - If this FIXME would have been a trivial exercise, I would have done it immediately. However, moving is only possible after some further changes in the simproc itself. - In the meantime, I did find time to address the issues (cf. bed063d0c526, 9979d64b8016 and b28dbb7a45d9) Lukas On 10/06/2012 04:12 PM, Florian Haftmann wrote: Hi all, I stumbled over some comments »(* FIXME: move to Set theory *)« in Finite_Set.thy. Note that with jEdit it is now really easy to edit the HOL theories interactively: isabelle build -b Pure&& isabelle jedit -l Pure So, you can get your intention done directly and need not to imitate the school book pattern »This is left as an exercise to the reader« ;-) Cheers, 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
Re: [isabelle-dev] Graphview
Hi Florian, Thanks for your feedback. The main developer Markus Kaiser is giving a presentation next week and we will discuss further steps. Here's a part of a private German discussion with Makarius that explains how to switch back to the classical browser (in PG/Emacs). in http://isabelle.in.tum.de/repos/isabelle/rev/7529c77ee92e ist nun alles erstmal integriert. Einige Sachen funktionieren aber noch nicht so glatt, z.B. ein voller class_deps graph von HOL/Main. Das eine oder andere Detail habe ich möglicherweise auch kaputt gemacht. Man kann in isabelle tty oder emacs mit der print mode option "-m graphview" das neue Tool aktivieren, sonst wird wie bisher der alte browser verwendet. Das gilt einheitlich für alle commands die intern auf display_graph basieren. Isabelle/jEdit verwendet stets Graphview in einem eigenen Dockable Window -- auch wenn das noch nicht Produktionsqualität erreicht. Lukas On 10/11/2012 01:31 PM, Florian Haftmann wrote: Hi all, the recently established graphview IMHO has currently two disadvantages: * Misfit of node annotation size wrt. to the size of the full graphs -- node annotations are not readable within a reasonable size coverage of the graph. * Does not scale well (e.g. class_deps from Main.thy). What are the plans for the next release? Graph browsing is a tool too vital that it can be set inoperative. Is there any chancing for improvements, or will there be a switch towards the classical browser alternatively? Cheers, 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
Re: [isabelle-dev] Hooks for postprocessing sessions!?
Hi Florian, this sounds similar to ideas that (Alex and) Lars had to allow find_theorems to search on all Isabelle sessions. As far as I know, they have an implementation for this feature in their shelf. Lukas On 10/11/2012 02:44 PM, Florian Haftmann wrote: Hi all, recently I had the idea to generate reports for all accessible Isabelle sessions containing e.g. * all constants (with types) declared in a session * all types declared in a session * all classes declared in a session * all theorems declared via »theorem« * ... The rationale is that this would allow for a quick analysis especially of the AFP to find out which generally useful »auxiliary« stuff is hidden there (e.g. http://afp.hg.sourceforge.net/hgweb/afp/afp/file/e9fa38f86b76/thys/Binomial-Heaps/SkewBinomialHeap.thy#l1643). Is there already feasible hook interface to hook in, e.g. in present.ML, or can this only be done by an ad-hoc patch? Cheers, 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
Re: [isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"
It is probably due to my latest changeset in the set_comprehension_pointfree simproc. Lukas On 10/10/2012 03:50 PM, Johannes Hölzl wrote: Hi, I tried to build AFP/Grith_Chormatic, but the simplifier fails in Ugraphs.thy line 168: using card_left_less_pair assms by simp with the following exception: exception THM 0 raised (line 790 of "drule.ML"): Ill-typed instantiation: Type ?'a ⇒ ?'b of variable ?f cannot be unified with type (?'a × ?'a) set ⇒ bool of term finite ?x = ?y ⟹ ?f ?x = ?f ?y There is no instantiation happening in the Isar text. Isabelle hg: 9a2a53be24a2, afp hg: 2b6348e4bda7, near the current tips. It seems to happen somewhere internal when instantiating card_left_less_pair. When I write using card_left_less_pair[of A] assms by simp it works. - Johannes ___ 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] Testboard [was: typedef (open) legacy]
On 10/10/2012 12:51 PM, Florian Haftmann wrote: I cannot connect to testboard at the moment, it seems to be in bad shape again. The testboard should now be in a running state again. For the record: is there any diagnosis what went wrong? On the webserver, spidermonkey was updated on Monday evening, and some changes were incompatible for couchdb. This caused couchdb to fail silently. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] typedef (open) legacy
On 10/09/2012 11:20 AM, Makarius wrote:
On Mon, 8 Oct 2012, Brian Huffman wrote:
I have a changeset that removes the set-definition features from the
{cpo,pcpo,domain}def commands in HOLCF, and it checks successfully on
testboard.
http://isabelle.in.tum.de/testboard/Isabelle/rev/a093798fa71b
Should I go ahead and push this changeset to the current tip?
I cannot connect to testboard at the moment, it seems to be in bad
shape again.
The testboard should now be in a running state again.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] strange behaviour with Z3 and smt method
Hi all, on the current Isabelle development version b2135b2730e8, I noticed a strange behavior with the smt proof method. It replies Solver z3: Z3 proof parser (line 87): unknown sort: "Bool" Although it is possible to work around it, it might be worthwhile to investigate. Lukas Z3_Bug.thy Description: application/isabelle-theory ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
On 09/24/2012 09:33 PM, Makarius wrote: On Fri, 21 Sep 2012, Lukas Bulwahn wrote: I am just at the moment trying to get it running again. Lukas On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote: Am 21.09.2012 um 09:18 schrieb Tobias Nipkow: The testboard runs most of the AFP. For the last three days, neither the tests nor testboard have been working. http://isabelle.in.tum.de/reports/Isabelle http://isabelle.in.tum.de/testboard/Isabelle Did you do anything, or did it come back by itself? I did restart a number of mira processes---the nagios tool from our sysadmin are monitoring them, so Lars and I get emails if they do not run anymore. Lukas In the meantime I also killed a number of inactive poly processes on the usual test machines. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
I am just at the moment trying to get it running again. Lukas On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote: Am 21.09.2012 um 09:18 schrieb Tobias Nipkow: The testboard runs most of the AFP. For the last three days, neither the tests nor testboard have been working. http://isabelle.in.tum.de/reports/Isabelle http://isabelle.in.tum.de/testboard/Isabelle Jasmin ___ 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] Fwd: status (AFP)
Thanks to Dmitriy's effort, all AFP entries run successfully again. Original Message Subject:status (AFP) Date: Fri, 21 Sep 2012 09:10:43 +0200 (CEST) From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle ) To: undisclosed-recipients:; The status of the following AFP entries changed or remains FAIL: [KBPs] changed from FAIL to ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id c3a75d6d802a Isabelle version: devel -- hg id 7bb0d515ccbc Test ended on: macbroy2, Fri Sep 21 09:10:43 CEST 2012. Have a nice day, isatest Stream-Fusion: ok Ramsey-Infinite: ok Binomial-Heaps: ok Ordinals_and_Cardinals: ok ClockSynchInst: ok Huffman: ok Completeness: ok Well_Quasi_Orders: ok Abstract-Hoare-Logics: ok Free-Boolean-Algebra: ok Stuttering_Equivalence: ok Girth_Chromatic: ok Valuation: ok FunWithFunctions: ok Coinductive: ok Heard_Of: ok Abstract-Rewriting: ok Matrix: ok POPLmark-deBruijn: ok MonoBoolTranAlgebra: ok FeatherweightJava: ok DiskPaxos: ok Free-Groups: ok Functional-Automata: ok GraphMarkingIBP: ok Transitive-Closure-II: ok Tycon: ok BytecodeLogicJmlTypes: ok Finger-Trees: ok WorkerWrapper: ok Separation_Algebra: ok General-Triangle: ok Program-Conflict-Analysis: ok LinearQuantifierElim: ok GenClock: ok Inductive_Confidentiality: ok Recursion-Theory-I: ok Efficient-Mergesort: ok BinarySearchTree: ok TLA: ok Lam-ml-Normalization: ok CoreC++: ok Marriage: ok Shivers-CFA: ok SATSolverVerification: ok Example-Submission: ok SumSquares: ok BDD: ok JiveDataStoreModel: ok Polynomials: ok Datatype_Order_Generator: ok Verified-Prover: ok Topology: ok KBPs: ok ArrowImpossibilityGS: ok Lazy-Lists-II: ok Locally-Nameless-Sigma: ok DataRefinementIBP: ok JinjaThreads: ok HRB-Slicing: ok DPT-SAT-Solver: ok RIPEMD-160-SPARK: ok Flyspeck-Tame: ok Regular-Sets: ok RSAPSS: ok LightweightJava: ok Gauss-Jordan-Elim-Fun: ok AVL-Trees: ok Category: ok AutoFocus-Stream: ok CofGroups: ok Perfect-Number-Thm: ok Depth-First-Search: ok Abortable_Linearizable_Modules: ok Statecharts: ok PseudoHoops: ok Max-Card-Matching: ok FunWithTilings: ok SenSocialChoice: ok CCS: ok List-Index: ok Markov_Models: ok Cauchy: ok Ordinal: ok Myhill-Nerode: ok Binomial-Queues: ok Fermat3_4: ok FOL-Fitting: ok MuchAdoAboutTwo: ok Slicing: ok Dijkstra_Shortest_Path: ok SIFPL: ok Presburger-Automata: ok Circus: ok Transitive-Closure: ok Impossible_Geometry: ok Category2: ok Integration: ok MiniML: ok NormByEval: ok PCF: ok SequentInvertibility: ok Pi_Calculus: ok FileRefinement: ok FFT: ok Robbins-Conjecture: ok Compiling-Exceptions-Correctly: ok Ordinary_Differential_Equations: ok VolpanoSmith: ok HotelKeyCards: ok Tree-Automata: ok FinFun: ok Psi_Calculi: ok Lower_Semicontinuous: ok Start test for /home/isatest/afp/devel at Fri Sep 21 06:31:44 CEST 2012, macbroy2 begin hg pull/update pulling from ssh://isat...@afp.hg.sourceforge.net/hgroot/afp/afp searching for changes adding changesets adding manifests adding file changes added 1 changesets with 1 changes to 1 files 1 files updated, 0 files merged, 0 files removed, 0 files unresolved remote: Running preoutgoing hook remote: Use of uninitialized value in concatenation (.) or string at /etc/mercurial/preoutgoing line 36. end hg pull/update AFP version: development -- hg id c3a75d6d802a Isabelle version: devel -- hg id 7bb0d515ccbc Building HOLCF ... Finished HOLCF (0:00:50 elapsed time, 0:01:01 cpu time, factor 1.22) Building HOL-Nominal ... Finished HOL-Nominal (0:00:21 elapsed time, 0:00:23 cpu time, factor 1.09) Building HOL-Multivariate_Analysis ... Finished HOL-Multivariate_Analysis (0:03:00 elapsed time, 0:06:32 cpu time, factor 2.17) Building HOL-Word ... Finished HOL-Word (0:00:38 elapsed time, 0:01:07 cpu time, factor 1.76) Building Jinja ... Finished Jinja (0:05:48 elapsed time, 0:13:16 cpu time, factor 2.28) Building LatticeProperties ... Finished LatticeProperties (0:00:20 elapsed time, 0:00:22 cpu time, factor 1.10) Building HOL-Probability ... Finished HOL-Probability (0:01:43 elapsed time, 0:03:24 cpu time, factor 1.98) Building Group-Ring-Module ... Finished Group-Ring-Module (0:03:22 elapsed time, 0:07:08 cpu time, factor 2.11) Building Simpl ... Finished Simpl (0:02:35 elapsed time, 0:04:55 cpu time, factor 1.90) Building Collections ... Finished Collections (0:05:32 elapsed time, 0:08:31 cpu time, factor 1.53) Building Refine_Monadic ... Finished Refine_Monadic (0:01:51 elapsed time, 0:02:51 cpu time, factor 1.54) Building List-Infinite ... Finished List-Infinite (0:00:45 elapsed time, 0:01:18 cpu time, factor 1.73) Building Nat-Interval-Logic ... Finished Nat-Interval-Logic (0:00:50 elapsed time, 0:01:19 cpu time, factor 1.58) Running Flyspeck-Tame ... Finished Flyspeck-Tame (0:03:12 elapsed time, 0:06:10 cpu time, factor 1.92) Running JinjaThreads ... Finished JinjaThreads (0:57:08 elapsed time, 1:51:07 cpu time, factor 1.94) Running HRB-Slicing ... Finished HRB-Slicing (0:05:54
[isabelle-dev] Thank you for all the great improvements
Hi all, I have just installed the Isabelle development repository on one of the remote machines. With the new build system, the component management and PolyML 5.5, I got a system up and running in less than 20 minutes. In former times, it usually took me 20 minutes just to get an updated Isabelle again working on some remote machine. I want to thank everyone involved for these great improvements. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Narrowing
On 07/28/2012 05:32 PM, Florian Haftmann wrote: Hi Lukas, I have corrected cs 6efff142bb54 by cs 7c497a239007, and have relaxed the issue with Efficient_Nat a little (cs 084cd758a8ab, see below for a short discussion). This has raised a couple of questions: 1. Why did the testboard not check this? Bad environment settings? I guess you are aware of the following issues to some extent, but also that your priorities are elsewhere at the moment. Nevertheless I would appreciate it if at one point in time you can return to them, maybe as joint work: Hi Florian, My priorities are indeed somewhere else. To give a few short answer to all your questions: 1. The testboard does not check it because ISABELLE_GHC probably is not set there. Maybe we could easily fix that. 2. The poking in generated code which happens in narrowing_generators.ML is highly discouraged and was the primary source for the breakdown in 6efff142bb54. It should be possible to get around without that using the code_include mechanism. 2. I tried out the code_include mechanism a while ago, but I could not succeed within half a day. There were other problems that were even worse than poking around. So I gave up and stayed with the current solution. We could give it another try if it's worth the effort. 3. The evaluation machinery for Haskell should be separate thing (maybe code_eval_haskell.ML), and also the communication could be less technically involved, e.g. a yxml output rather than invoking the SML compiler right after the Haskell compiler just to parse something. 3. I thought of this as well, but did not find another prime application besides Quickcheck. That's why the mechanism is still in the module Quickcheck-Narrowing. 4. After 084cd758a8ab, Efficient_Nat works in principle, but there are other problems: * the type ambiguity inference seems not to work as expected * there is no term_of equation for nat * … I did not dive into detail here, because all these must be treated at a glance. I guess the term_of issue can be dealt with as soon as Efficient_Nat uses a different architecture. Another issue is that we really need to understand what a generic Haskell evaluation machinery consists of. 4. I cannot comment on that. 5. There are still all those funny sequence theories in HOL (New_Foo_Sequence) which are awaiting cleanup. 5. That's true. I will get rid of them soon. 6. What I so far have not been aware of is that in Haskell there are always multiple modules (one module =^= one file), contrary to ML and Scala. I think at some stage I have to make this more explicit in the overall architecture. 6. I see. Okay, that's the reason, why some modes of the code generator produce non-compilable files after some reasonable code setup. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Comment in Efficient_Nat
On 07/22/2012 10:29 AM, Florian Haftmann wrote:
text {*
FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
@{text "code_module"} is very aggressive leading to bad Haskell code.
Therefore, we simply deactivate the narrowing-based quickcheck from here on.
*}
I do not unserstand this. What does "code_module" mean here? And why
is it aggressive?
I do recall not the exact details anymore. But I believe that the setup
with "code_modulename" caused the narrowing-based quickcheck to produce
non-executable code.
(If I remember correctly, it produced one file with multiple modules,
which is not valid Haskell code. code_modulename was just to aggressive.)
If you are looking into this and would fix it, that would be great. We
can discuss the details offline.
Probably related, with the changeset 6efff142bb54, the narrowing-based
quickcheck fails to generate valid code.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] AFP tests timing out
Hi all, for about one month now, we are continuously seeing the AFP tests failing on various entries because of timeouts, e.g. AVL-Trees, Regular-Sets, Collections. To my knowledge, the entries have not changed. So the timeouts seem to be caused by recent changes in the Isabelle system itself. @Alex: Could you provide graphs of the runtime for the AFP of the last few weeks to identify the possibly critical changesets? @all: Are there some educated guesses what could have changed the performance on all these theories? Should we ignore the performance drop and simply increase the timeouts on these sessions? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] status (AFP)
Hi all, since 06/05/2012, I have not received any status (AFP) emails, although it should have been failing the last days. (After Isabelle:e7e647949c95, the theory LinearQuantifierElim was failing, and I just fixed with AFP:96f043cb412e.) Is the AFP test script still working properly? Maybe latest changes to the contrib directories broke the test script? Lukas On 06/05/2012 09:51 AM, Isabelle wrote: The status of the following AFP entries changed or remains FAIL: [JinjaThreads] changed from FAIL to ok. Full entry status at http://afp.sourceforge.net/status.shtml AFP version: development -- hg id 4c44fdeca962 Isabelle version: devel -- hg id 72acba14c12b Test ended on: macbroy2, Tue Jun 5 09:51:34 CEST 2012. Have a nice day, isatest ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] new quick check expriment
On 06/17/2012 06:36 PM, Florian Haftmann wrote: Thanks. It asks me to set 'Environment variable ISABELLE_GHC '. So I uncomment the line 'ISABELLE_GHC="/usr/local/ghc/$ISABELLE_PLATFORM/ghc' Now it gives me another error message "Compilation with GHC failed". Any suggestion ? PS, I work in a mac version of Isabelle 2012 Maybe we have to find a way to provide ghc as a component also… Although Haskell is an essential part for Quickcheck in Isabelle and it would simplify the installation process for Quickcheck, I am not in favour to provide ghc contributed with the Isabelle distribution. So GHC must be installed by the usual means of the operating system, e.g., through some package manager. Providing GHC as a component might try to help to install GHC on the operating system, or could try to detect the path of GHC automagically, but I do not have a clear vision how this should work. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On 05/30/2012 02:44 PM, Makarius wrote: On Wed, 30 May 2012, Lukas Bulwahn wrote: On 05/29/2012 02:01 PM, Makarius wrote: * Admin/contributed_components within the repository documents semi-formally which components may be included into a certain version. The mira experts should be able to say more about the current used of that file in the testing framework. Roaring ahead with the grand unified contrib, I guess someone has changed the Scala version on lxbroy10, because now the Scala export with Imperative-HOL fails on lxbroy10. The interesting bit of information is actually here: http://isabelle.in.tum.de/reports/Isabelle/report/78fa8d673aac4dcca02465b91815adb9#l260 env: /tmp/mira/workbench/62527-140537428690688/Isabelle/contrib/scala-2.9.2/bin/scalac: Permission denied Which was caused by the lack of group executablity for the scala/bin files, which I have changed now. Thank you for digging deeper into this. So the mira testing should be now back to a working state. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
On 05/29/2012 02:01 PM, Makarius wrote: * Admin/contributed_components within the repository documents semi-formally which components may be included into a certain version. The mira experts should be able to say more about the current used of that file in the testing framework. Roaring ahead with the grand unified contrib, I guess someone has changed the Scala version on lxbroy10, because now the Scala export with Imperative-HOL fails on lxbroy10. Does anyone feel responsible? Maybe it only requires a few tweaks in the code generation setup to adjust to the new version. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 05/25/2012 03:31 PM, Lukas Bulwahn wrote: On 05/25/2012 02:17 PM, Makarius wrote: On Fri, 25 May 2012, Lukas Bulwahn wrote: On 05/23/2012 01:28 PM, Makarius wrote: Dear All, the current situation is as follows: * As of Isabelle/c5f7be4a1734 the http://isabelle.in.tum.de/repos/isabelle-release branch is merged again with the main line. * isatest is back testing http://isabelle.in.tum.de/repos/isabelle With the mira testing, Isabelle-makeall on lxbroy10 seems to be not terminating after the release branch was merged back. I killed the processes now throughout the days, but I cannot tell what the error is. It seems as if the script "perl -w /lib/scripts/feeder.pl" is doing something wrong. This is really odd. From the description it can only be a consequence of this change from the isabelle-release repository: changeset: 47868:32c03d45fffe user:wenzelm date:Fri May 04 17:14:42 2012 +0200 files: lib/scripts/feeder.pl description: refrain from SIGHUP handling (cf. 5f629ee2502b), which does not work on Cygwin and appears to be redundant anyway (no extra output produced within pipe); It is a bit disturbing that the grand-unified Larry Wall operating system no longer works reliably. I am able to see isatest/mira processes on lxbroy10 where certain perl processes "hang", i.e. cannot be killed via SIGHUP as expected (but SIGTERM works). So far I have been unable to reproduce the behaviour in isolation. It might somehow depend on the precise options of mira. I've tried to get them from Admin/mira.py without success. What are the precises ML_OPTIONS and ISABELLE_USEDIR_OPTIONS here? They are the "default" options, but I do not know how they are detected (your bash scripts?) and how to get this information. Lukas Your attempt, changeset 6de952f4069f, was successful. lxbroy10 now can test all future changesets again. Unfortunately, once mira tests older changesets it hangs, so all developers should please push to the testboard, tell me, and I will restart the daemon. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle2012 post-release mode
On 05/23/2012 01:28 PM, Makarius wrote: Dear All, the current situation is as follows: * As of Isabelle/c5f7be4a1734 the http://isabelle.in.tum.de/repos/isabelle-release branch is merged again with the main line. * isatest is back testing http://isabelle.in.tum.de/repos/isabelle With the mira testing, Isabelle-makeall on lxbroy10 seems to be not terminating after the release branch was merged back. I killed the processes now throughout the days, but I cannot tell what the error is. It seems as if the script "perl -w /lib/scripts/feeder.pl" is doing something wrong. The report on https://isabelle.in.tum.de/testboard/Isabelle/report/113b081700754f768fe458e15cd460a1 and http://isabelle.in.tum.de/testboard/Isabelle/report/7950b174d6e340aba223611991c32ec6 show some error messages, but they are not very informative. Any hints are welcome. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nominal and FinFuns from the AFP
Hi Christian, For code generation purposes and especially Quickcheck, it is necessary that the FinFun theory would be imported by any user. With the new developments lifting and transfer, we are getting very close that FinFun can be used without any further ado. I do have some latest experiments and patches in the shelf to be published after the release. Therefore, I am also in strong favour for moving the AFP entry FinFun into the distribution. In the long run, it should probably even become part of the HOL-Main image. In the short term, we could move the FinFun theory into the HOL library of the development version after Isabelle 2012 and the AFP 2012 has been released, if we agree that this moves this contribution in the right direction. As Andreas has access to the Isabelle development and can freely change and contribute the entry, I do not see any further difficulties. Lukas P.S.: The topic is interesting for isabelle-users as well in my opinion. On 05/10/2012 05:09 PM, Christian Urban wrote: Dear All, In Nominal I am usually relying on types that are defined in HOL or that I define myself. However, I now came across the FinFun development in the AFP by Andreas Lochbihler (thanks to Larry). The finfun type seems to be rather useful to Nominal users, since it has finite support, in contrast to the function type, which in general hasn't. My question is how I should I interface with something that is in the AFP and with something that is (eventually) in the distribution? The problem is that Nominal always needs a wrapper infrastructure for types, such as a definition of a permutation. How should I write this wrapper, especially what should the import paths be, so that users can conveniently use FinFuns and Nominal? Should this wrapper be part of the AFP entry (in which case the paths are clear, but then Nominal users have to fetch the AFP explicitly and no Nominal example in the distribution can depend on it)? Or should the wrapper be part of Nominal (in which case I can use it in examples, but I have no idea what the import paths should be...the AFP can be anywhere)? Or, should FinFun be part of the distribution (which would make my life normal again)? Is there any received wisdom for this problem? Best wishes, Christian ___ 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] Tweak Haskell output for future Haskell compatibility.
On 05/08/2012 01:49 PM, Peter Lammich wrote:
On Di, 2012-05-08 at 12:55 +0200, Tobias Nipkow wrote:
Am 08/05/2012 12:41, schrieb Makarius:
On Tue, 8 May 2012, Tobias Nipkow wrote:
I mean the datatype definition facility.
Over the years this lead to occasional confusion of end-users, who wanted to
restrict their datatype constructors on purpose. (I can dig up an email by
Elsa Gunter from the late 1990-ies, if you want.)
It is precisely such a convincing example I am looking for. It seems to me
that such constraints restrict the types artificially: the type makes sense
without it. What is gained by the constraint?
Foundationally nothing, which is why constraints are not present in most of the
raw definitional primitives, at the bottom of the logic.
There is a difference of the foundation vs. the user context, though. (As usual
"user" means other packages or end-users connected to the surface syntax of such
packages.) The Isabelle experts in the background have spent countless years to
make all this work most of the time, such that it is rarely visible now where
things actually happen, and how.
Kudos to the experts, but my question was *why* the type constraints are
supported for dataypes. What is the use case?
One use case arises in imperative HOL, where you want to declare
datatypes that can be stored on the heap, and thus, they only make sense
if constrained to ::heap - sort. E.g.
datatype a'::heap linked_list = nil | node 'a "'a linked_list ref"
Currently, Imperative/HOL does some ML-magic after the datatype
declarations here, which certainly looks much cleaner when just adding a
sort constraint.
The mentioned ML-magic achieves two things:
First, you want to restrict 'a to be constrained to heap in the phantom
type:
datatype ('a :: heap) ref = Ref nat
Second, when defining linked lists, the restriction has to be dropped
locally,
as "valid" (user-space) type definition would require to prove the
datatype "'a node" being of sort heap interleaved with its definition in:
datatype 'a node = Empty | Node 'a "('a node) ref"
Maybe with new developments can this be achieved written in a more
"user-friendly" way, although understanding one line of ML is the least
problem in the overall confusion of this subject.
It is actually more surprising that sort constraints are imposed
(however only for convience, and not because of foundational reasons)
and can be dropped if one wishes at any point.
Lukas
Peter
Tobias
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
___
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] isatest home directory full
On 04/22/2012 03:04 PM, Florian Haftmann wrote: I've managed to remove more than 5 GB of old heap files, but this might be a bit pathethic due to this directory: 225G tmp/shared_results Does anybody know what it is? These are the results from the mira runs, which in theory are kept eternally. There is the mira command »purge« which throws them away except the most recent ones (however the heuristic is). I personally don't have any intimate knowledge about the mira setup at TUM any longer and am reluctant to risk something, so I kindly ask for action from the current mira administrators at TUM. Best, Florian We manually purge the results when we get close to the quota. This is now been done just a moment ago. Supposingly our quota is monitored, and we should get email notifications, however I have not seen any lately. Lukas ___ 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] Quickcheck Examples
On 04/20/2012 02:12 PM, Lukas Bulwahn wrote: On 02/27/2012 02:31 PM, Makarius wrote: On Mon, 27 Feb 2012, Lukas Bulwahn wrote: A large part of Quickcheck's run time is spent in the code generator calls, and the evaluation, which does mostly memory allocations and deallocations. I am surprised that this issue suddenly occurs now that it is its own session. Maybe the many parallel invocations of Quickcheck now pressure the ML compiler much more than as it was just a part of HOL-ex. In principle the codegen infrastructure and all should work in parallel, but there might be additional oddities in the quickcheck scenario. You can reproduce the presumed non-termination on macbroy2 with regular settings like this: ISABELLE_USEDIR_OPTIONS=-i false -d false -M 4 -q 2 ML_PLATFORM=x86_64-darwin ML_HOME=/home/polyml/polyml-5.4.1/x86_64-darwin ML_SYSTEM=polyml-5.4.1 ML_OPTIONS=-H 1000 --gcthreads 4 The process is running with approx. 100-200% most of the time, which is neither sequential nor fully parallel. Probably you merely benefit from theory parallelism, not from more fine-grained Par_List things that could be used in your own code. One potential source of problems is the pseudo-random generator, with its global state. There have been funny effects in the past that might have come back in one form or the other, even though random generators have been changed several times. Anyway, how long does the session run on "your laptop"? I have not noticed that non-termination on my laptop when checking my changesets. Also with the setting mentioned above, I could not reproduce the non-terminating behaviour on macbroy2 with changesets baf90cb2a606. I was mistaken--I was checking with f5eaa7fa8d72. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On 02/27/2012 02:31 PM, Makarius wrote: On Mon, 27 Feb 2012, Lukas Bulwahn wrote: A large part of Quickcheck's run time is spent in the code generator calls, and the evaluation, which does mostly memory allocations and deallocations. I am surprised that this issue suddenly occurs now that it is its own session. Maybe the many parallel invocations of Quickcheck now pressure the ML compiler much more than as it was just a part of HOL-ex. In principle the codegen infrastructure and all should work in parallel, but there might be additional oddities in the quickcheck scenario. You can reproduce the presumed non-termination on macbroy2 with regular settings like this: ISABELLE_USEDIR_OPTIONS=-i false -d false -M 4 -q 2 ML_PLATFORM=x86_64-darwin ML_HOME=/home/polyml/polyml-5.4.1/x86_64-darwin ML_SYSTEM=polyml-5.4.1 ML_OPTIONS=-H 1000 --gcthreads 4 The process is running with approx. 100-200% most of the time, which is neither sequential nor fully parallel. Probably you merely benefit from theory parallelism, not from more fine-grained Par_List things that could be used in your own code. One potential source of problems is the pseudo-random generator, with its global state. There have been funny effects in the past that might have come back in one form or the other, even though random generators have been changed several times. Anyway, how long does the session run on "your laptop"? I have not noticed that non-termination on my laptop when checking my changesets. Also with the setting mentioned above, I could not reproduce the non-terminating behaviour on macbroy2 with changesets baf90cb2a606. I will continue testing Quickcheck-Examples to see if it only occurs infrequently. Can you other system configurations by running the isatest with the "full" target? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
On 04/18/2012 08:26 PM, Florian Haftmann wrote: Hi all, - I would like to add a size limit to records beyond which no code generator setup is performed. The main reason is that on sizes> 200 fields or so, the setup does not make any sense, but consumes very large amounts of memory (and time). Switching it off gets rid of almost all of the mysterious memory blowup that we had and enables us to run our proofs within 4GB on Linux (32bit) and ~8GB on Darwin (64bit). Having limits like these is not ideal, but I don't see a better workaround, because the code generator setup *is* useful for small records. There is a question on how to implement the limit: 1) as an option available the user at record definition time 2) as an option/flag to the internal record definition function only 3) as a configuration option 4) as a compile time constant There is a third small thing that I will discuss separately with Florian: there is a bug in the code generator setup in Isabelle2011-1 somewhere in generating narrowing lemmas. It is triggered for records with more than ~530 fields where it constructs a lemma of the form "f ty = g a b .. aa ab .. tw tx ty tz .." where the ty on the rhs is different to the ty on the left. It should be easy to fix once I manage to trace down where it is actually constructed and I haven't checked yet if it still occurs in the development version. I think it is very important to differentiate here into more detail. There is not »the« code generator setup but a layered one: a) Registering a record, its projections and quality on the record as an executable program fragment b) Provided support for all those funny quickcheck generators. I would strongly recommend not to sacrifice a) for a »optimisiation« (once I had something similar in the datatype package and it produced a lot of pain); basically, it uses theorems which are »almost there« anyway. What happens in b) is much more ambitious, and if this is really a bottleneck, an option like »record_quickcheck« could do the job. But I think before to settle here it is important to have more detailed benchmarks about records which separates figures for a) and b). Commenting out ensure_random_record and ensure_exhaustive_record in function add_code coulde make a good start. Undoubtedly, Quickcheck has to produce a few "large terms" for each record to support them. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
On 04/16/2012 09:13 AM, Christian Sternagel wrote: Hi all, On 04/03/2012 02:51 AM, Florian Haftmann wrote: well, I suggest to augment the existing theory with lemmas transferred from relpow to relpowp to emphasize that both worlds exists and that lemmas can be found easier by find_theorems. The typical pattern is lemma foo_relpow: ... lemma foo_relpowp: ... by (fact foo_relpow [to_pred]) I did this in the meantime (tested with "isabelle makeall all"). This time as a patch (in order to avoid cluttering the history) on Theory Transitive_Closure. Suggested NEWS entry: -- * Theory Transitive_Closure: Duplicated facts about "relpow" for "relpowp" to emphasize that both worlds exist and facilitate better results with "find_theorems". Added Lemmas: relpowp_1 relpowp_0_I relpowp_Suc_I relpowp_Suc_I2 relpowp_0_E relpowp_Suc_E relpowp_E relpowp_Suc_D2 relpowp_Suc_E2 relpowp_Suc_D2' relpowp_E2 relpowp_add relpowp_commute relpowp_bot rtranclp_imp_Sup_relpowp relpowp_imp_rtranclp rtranclp_is_Sup_relpowp rtranclp_power tranclp_power rtranclp_imp_relpowp relpowp_fun_conv -- I pushed your changes to the public repository, but I did not consider the NEWS entry worth mentioning -- we add theorems on a daily basis, without explicitly advertising them in the NEWS. Lukas cheers chris ___ 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] Relations vs. Predicates
On 04/16/2012 09:13 AM, Christian Sternagel wrote: Hi all, On 04/03/2012 02:51 AM, Florian Haftmann wrote: well, I suggest to augment the existing theory with lemmas transferred from relpow to relpowp to emphasize that both worlds exists and that lemmas can be found easier by find_theorems. The typical pattern is lemma foo_relpow: ... lemma foo_relpowp: ... by (fact foo_relpow [to_pred]) I did this in the meantime (tested with "isabelle makeall all"). This time as a patch (in order to avoid cluttering the history) on Theory Transitive_Closure. Suggested NEWS entry: I am testing it again, cf. http://isabelle.in.tum.de/testboard/Isabelle/rev/74e9843f7aae Lukas -- * Theory Transitive_Closure: Duplicated facts about "relpow" for "relpowp" to emphasize that both worlds exist and facilitate better results with "find_theorems". Added Lemmas: relpowp_1 relpowp_0_I relpowp_Suc_I relpowp_Suc_I2 relpowp_0_E relpowp_Suc_E relpowp_E relpowp_Suc_D2 relpowp_Suc_E2 relpowp_Suc_D2' relpowp_E2 relpowp_add relpowp_commute relpowp_bot rtranclp_imp_Sup_relpowp relpowp_imp_rtranclp rtranclp_is_Sup_relpowp rtranclp_power tranclp_power rtranclp_imp_relpowp relpowp_fun_conv -- cheers chris ___ 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] Towards the next release
On 04/12/2012 08:32 PM, Makarius wrote: On Thu, 12 Apr 2012, Lukas Bulwahn wrote: We still have the locale browser in the pipeline. Do you have objections to integrate the tool you have reviewed two months ago? Our private discussion yielded further source code improvements, however the tool is already in a fully functional state, and the source code improvements would not change so much from a user's point of view. I remember well our discussion with Stefan Berghofer and especially Markus Kaiser who did the main work in this project. We parted at the point where everybody observed the little return that JUNG gives for all the investment that it requires. This huge "framework" also seems to be unmaintained since 2010, exactly at the moment when I was getting excited about it (errornously). After removing all the initial hopes what JUNG would deliver, only two potential benefits were remaining on our list: (1) Java object model for graph data structures (2) facilities for drawing and a bit of editing of graphs You had pointed out that a port of the Isabelle graph.ML to Scala would make (1) obsolete (which has its own problems due to mutability). I did that in the meantime, and made various refinements so that http://isabelle.in.tum.de/repos/isabelle/file/83294cd0e7ee/src/Pure/General/graph.scala is pretty stable and closely agrees with the ML version. I am already using graph.scala myself in the Prover IDE document model, to manage dependencies of theory buffers etc. Since (2) is nothing specifically exciting by JUNG either -- it seems to be based on plain Java Graphics2D stuff -- I had recommended to abandon JUNG altogether. Did anything happen here in the meantime? We have discussed internally in more detail how to continue, but have not made any progress in the implementation itself. I have also spoken to Stefan Berghofer again, and encoraged him to help porting his great graph layout tool to Scala. Conceptually, the old graph browser can still compete with newer things on the market, but with its use of AWT from Java 1.1 that is hard to explain to end-users. (It is also technically hard to integrate into contemporary Swing components.) Before Stefan starts yet another implementation, we should make sure that the different projects converge. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Makarius, Hi Chris, On 04/12/2012 08:12 PM, Makarius wrote: On Wed, 11 Apr 2012, Christian Sternagel wrote: On 04/05/2012 12:30 PM, Christian Sternagel wrote: Hi Lukas, thanks for testing! (Sorry for the late reply, currently my internet-connectivity is rather sporadic ;)). Please find attached a hg bundle that does the name change 'rel_comp -> relcomp' for the AFP. It seems that Lukas has now pushed that, see Isabelle/d8fad618a67a I was expecting that someone else who also feels responsible for names of the base theories would comment on the changes, but nobody did. So, I did not have the patience to wait any longer and pushed the changes. If anyone present, for any reason knows why these two changesets should not be merged, let him speak now or forever hold his peace. I now also know who this mysterious "griff" from AFP is :-) Seriously, you have the free choice to specify your user name for Isabelle hg contributions, but you need to stick to it in the long run. In the initial warmup-phase you have one chance to rethink the initial choice, but do not have to do so. Is something wrong with my changesets? ;) You are an experienced Mercurial user already, so there are few technical things to say here. Semantically, the principles in the (slightly long) file README_REPOSITORY of the Isabelle repository apply, even when things are pushed by an intermediary person with administrative push access (the latter is also resposible to inspect incoming things in this respect). In the explanations there is a section about merges with a few important hints: * Accumulate private commits for a maximum of 1-3 days. ... * Test the merged result as usual and push back in real time. Piling private changes and public merges longer than 0.5-2 hours is apt to produce some mess when pushing eventually! Since your changes 07f4bf913230 and b75ce48a93ee were a bit too long stuck in the pipeline, you then had a non-trivial merge in e1b761c216ac. It seems that Lukus did not want to redo that via a variant of "rebasing" (e.g. plain "hg import" of individual changesets on tip), so he re-merged the whole thing with his current tip in d8fad618a67a and then pushed it. I tried to do the rebase, but as the merge was non-trivial, the rebasing would have taken again quite some time, so I risked having a long edge in the repository graph instead. I guess for the future, especially external contributions should provide patches without merges, but instead make sure that the patches can be applied to "the current tip" (even though this requires some maintenance from the contributor while internals are reviewing the changeset). Isn't it nice what the history of Mercurial tells? When producing the history one also needs to keep readability and clarity in mind -- it needs to be studied routinely when sorting out problems. Moreover, incoming changesets needs to be easy to inspect in a few seconds or minutes. (This is why I always ask to write each log item on a separate line, but still with a delimiter such as ";"). Nothing bad happened despite all these static type errors in the above changes, nonetheless one needs to maintain a routine of "correctness by construction" of Isabelle history. Over the years, I had occasionally spent several hours or days (or rather nights) trying to disentangle unclear situations for particularly odd changesets. In the commits, I only checked the "very minimal" requirements, although as you mention, there are many many aspects for future changesets that can be improved. I still awaiting a good NEWS entry from Chris. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards the next release
On 04/12/2012 11:02 AM, Makarius wrote: Dear all, we need to get to a more concrete release schedule. Presently I would like to aim for late May, which means we need to start consolidating and converging about now. Are there any further big things in the pipeline? We still have the locale browser in the pipeline. Do you have objections to integrate the tool you have reviewed two months ago? Our private discussion yielded further source code improvements, however the tool is already in a fully functional state, and the source code improvements would not change so much from a user's point of view. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Spare cycles on compute server
Hi all, our system administrators just told me that our Munich compute server (lxbroy10) still has many spare cycles, which we could use for more testing and other measurements. At the moment, there are two processes: one checking isabelle_makeall on the testboard, another checking AFP_fast on the testboard. Any suggestions what we should test more? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Relations vs. Predicates
Hi Chris, I have tested your changeset on the testboard, and a couple of AFP theories break, cf. http://isabelle.in.tum.de/testboard/Isabelle/report/edd1df5c8daf4109a6366801aaeff7fd (Some errors are due to your changes, some are due to current work of others.) It might be good to provide some patches for the AFP to have a smooth transition. Lukas On 04/04/2012 09:20 AM, Christian Sternagel wrote: Hi all, On 03/31/2012 01:10 AM, Florian Haftmann wrote: PS: I suggest to rename "rel_comp" into "relcomp" (to be consistent with "relpow"). This would also mean to rename the corresponding lemmas, although I would also appreciate consistency. Also the »pred_comp« abbreviation should be dropped, with the subsequent consequences for theorem names. This would also be something you could contribute if you like. The attached hg bundle contains the renaming from "rel_comp" to "relcomp," and replaces all occurances (also in lemma names) of the abbreviation "pred_comp" by "relcompp." I tested the bundle (with "isabelle makeall all") against changeset e1b761c216ac. Only HOL-Metis_Examples failed. Could this failure be due to the fact that my machine only uses remote_ versions of ATPs. Or is this really related to my change? (Currently I don't see how.) cheers chris ___ 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] Isatest
The webpage on the Isabelle (community) wiki, https://isabelle.in.tum.de/community/Administration_of_the_isatest_facilities, summarizes the agreement of this thread. If anyone wants to add or modify the page, feel free to do so. Lukas On 03/29/2012 09:29 AM, Gerwin Klein wrote: On 29/03/2012, at 4:31 PM, Tobias Nipkow wrote: Am 28/03/2012 23:30, schrieb Gerwin Klein: On 29/03/2012, at 6:11 AM, Makarius wrote: On Wed, 28 Mar 2012, Florian Haftmann wrote: Once there has been the idea that everyone having commit access to the Isabelle master repository (POSIX group isabelle at nfsbroy) is also a isatest subscriber. Maybe it would be helpful to establish this as a rule (at least of thumb). Isatest mails can still be sorted out by local email filters. What do you think? I could imagine some reforms in the meaning of the Unix group "isabelle" and how it is managed, although I have a tendency to leave the status-quo untouched. For every administrative facility that is added, one also needs to take maintenance into account. Yes, that is the main problem I see with this (otherwise I'm all for it). If there is an email list that automatically contains everyone with push-access, emails could easily be sent there. I wouldn't want to have to maintain that email list, tough. Florian suggested "a rule (of thumb)", not automation. Hence I am still in favour. It just means that whoever grants write access should try and remember to add that person to the email list. As long as I don't have to do anything for each entry/exit, I'm easy. The list is controlled via the settings in the repository, so anyone in the group can add/remove people. Cheers, Gerwin ___ 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] JDK / Mira
I restarted all mira daemons now. Lukas On 03/29/2012 09:53 AM, Florian Haftmann wrote: I guess someone must restart the mira deamons in order to run with the adjusted configurations. 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] Building the IsarImplementation Manual on 9fc17f9ccd6c
I cannot build the IsarImplementation Manual on 9fc17f9ccd6c: Maybe some latest change broke the document generation. Lukas Running HOL-Thy ... HOL-Thy FAILED (see also /home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy) *** *** The error(s) above occurred in document antiquotation: "Base.index_ML" (line 130 of "~~/doc-src/IsarImplementation/Thy/Logic.thy") *** At command "text" (line 118 of "~~/doc-src/IsarImplementation/Thy/Logic.thy") *** Error: *** Type mismatch in type constraint. ***Value: Name_Space.declare : *** Context.generic -> *** bool -> binding -> Name_Space.T -> string * Name_Space.T ***Constraint: ***Proof.context -> ***bool -> ***Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T ***Reason: ***Can't unify Context.generic with Proof.context *** (Different type constructors) *** *** The error(s) above occurred in document antiquotation: "Base.index_ML" (line 1109 of "~~/doc-src/IsarImplementation/Thy/Prelim.thy") *** At command "text" (line 1089 of "~~/doc-src/IsarImplementation/Thy/Prelim.thy") Exception- TOPLEVEL_ERROR raised *** ML error make: *** [/home/bulwahn/.isabelle/./heaps/polyml-5.3.0_x86-linux/log/HOL-Thy.gz] Error 1 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Name for derived quotient_def theorem
Hi Florian, Thank you for your suggestions. We will take them into account. On 03/28/2012 07:26 AM, Florian Haftmann wrote: http://isabelle.in.tum.de/reports/Isabelle/rev/861f53bd95fe#l1.53 the name given to the derived theorem is unsatisfactory. Since it is not a »code-only« theorem, it should not carry the »code« within. If it would be a »code-only« theorem, the convention is to suffix with »_code«, not »_code_eqn«. Also, for derived theorems proved by packages it is much more common to use qualification suffixes (e.g. ».simp«, ».intro«) rather than plumbing underscores (cf. module binding.ML). Btw. this also applies to the respectfulness theorem: ».rsp« would be better than »_rsp«. This is explained by looking at the history: The typedef package introduces names with underscores, quotient_type and quotient_def inherit this from typedef. Here a list of names we were thinking of while discussing: - abstract_eq - abs_equation - abs_def - code_cert - code_certificate In the end, we decided for the one you can see (although I am personally still in favor of abs_equation or similar). I think ".simp" is rather strange, because it is really not simplifying anything, but rather unfolding the definition in some special way. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: numeral representation
On 03/26/2012 02:10 PM, Makarius wrote: On Sun, 25 Mar 2012, Brian Huffman wrote: As of 2a1953f0d20d, Isabelle now has a new representation for binary numerals Execellent, this is a big step forward in this important reform. It seems we now have the main parts in place, so that we can start consolidating towards the release over a couple of weeks. (I am still unsure myself, when the release point will be precisely.) Another pending issue of 2a1953f0d20d is HOL-Proofs-Lambda. When run in parallel it fills up > 25 GB of memory on my 32 GB machine. When run in x86 mode, it runs out of stack on polyml-5.4.1. The critical spot might be a definition of datatype or datatype realizer. This needs further investigation. Do you have any ideas on the spot? This problem is reproducible on our testboard servers. At the moment, all tests of changesets after 2a1953f0d20d have to be manually aborted because of that reason. I hope you find a solution quickly, otherwise we should deactivate the Proofs-Lambda theory to keep a stable testing environment. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/23/2012 11:45 AM, Jesus Aransay wrote: I know there is an alternative way to get that, by means of sparse matrices (SparseMatrix.thy), but it demands translating every operation over the matrix type to its equivalent version for "sparse matrices", which may be sometimes hard work. Code generation often requires translating or transfering every operation from one type to another. At the moment, users have to do this manually (which can be hard work as you said), but we are working on a mechanism that should soon automate this. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 09:08 AM, Christian Sternagel wrote:
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
"op |> = {(x, y). supt_impl x y}"
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum
instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of "op |>" on the type "...
set". To execute this, you have to move this specification to predicates
('a => bool):
Define "op |> = (%(x, y). supt_impl x y)"
Lukas
Sorry I don't quite get it. op |> is already defined to be of type
"('f, 'v) term rel" (and used heavily as a set). So the above equation
would not be well-typed. Is your suggestion to change op |> into a
predicate?
cheers
chris
Yes.
If you have an infinite set during the execution in the generated code,
which you hinted at before, you cannot use the type 'a set for code
generation, but you must use 'a => bool.
I cannot estimate how much work that is in your case.
If it is unfeasible in your formalisation to change this, there might
also be other means to obtain an executable specification by creating an
alternative data refinement for sets, but I only had this in the back of
my mind, and we have not done this (yet).
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
"op |> = {(x, y). supt_impl x y}"
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of "op |>" on the type "...
set". To execute this, you have to move this specification to predicates
('a => bool):
Define "op |> = (%(x, y). supt_impl x y)"
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Status of AFP/JinjaThreads
I fixed the proof in JinjaThreads with changeset 78eb9266adb0. However, due to the deeper reason that the classical reasoner setup has been changed so that the original proof failed, one might have to look into this specific subgoal again (understanding how the classical reasoner has been changed). (I am guessing it is due to the Predicate/Relation intro/elim changes.) Lukas On 03/19/2012 01:53 PM, Makarius wrote: Dear all, as of Isabelle/1d8601c642cc and AFP/039e21d114f1 the situation with JinjaThreads is better than it used to be, but it still fails. The critical bit is here: *** Failed to finish proof *** At command "by" (line 1123 of "thys/JinjaThreads/Execute/Scheduler.thy") It looks like a casualty of recent changes with 'a set, lattice, inductive_set, numerals or similar. This part of the session can be checked easily with only 2 cores and a few GB of memory. So maybe someone who feels responsible for recent changes in main HOL could take a look at it. 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] Fwd: status (AFP)
I hope changeset 2cdf5c71b818 in the AFP solves the issue. Lukas On 03/11/2012 01:02 PM, Brian Huffman wrote: On Sun, Mar 11, 2012 at 12:09 PM, Tobias Nipkow wrote: One error in JinjaThreads was fixed, here is the next one: *** Unknown fact "list_all2_update_cong2" (line 467 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy") *** At command "apply" (line 467 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy") Exception- TOPLEVEL_ERROR raised I guess this has to do with the following changeset: changeset: 46665:c1d2ab32174a user:bulwahn date:Sat Feb 25 09:07:37 2012 +0100 summary: one general list_all2_update_cong instead of two special ones http://isabelle.in.tum.de/repos/isabelle/rev/c1d2ab32174a ___ 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] Quickcheck Examples
Thanks a lot for your help. A large part of Quickcheck's run time is spent in the code generator calls, and the evaluation, which does mostly memory allocations and deallocations. I am surprised that this issue suddenly occurs now that it is its own session. Maybe the many parallel invocations of Quickcheck now pressure the ML compiler much more than as it was just a part of HOL-ex. Lukas On 02/27/2012 12:22 PM, Makarius wrote: There are further problems with HOL-Quickcheck_Examples. In recent repository versions it does not terminate so well -- I've stopped trying after approx. 1h CPU time. (Aside: judicious use of Par_List operations could improve quickcheck tools significantly.) The removal of Find_Unused_Assms_Examples in b07ae33cc459 does not help either. In fact it is a bad idea to leave untested things in the repository, they will start to rot and to smell rather quickly. So in 879f5c76ffb6 I've now moved the whole problem session to the "full" target of the IsaMakefile. This is only run by some isolated isatest sessions, probably not mira. This gives the opportunity to isolate all these issues, without degrading productivity of everybody else. (The makeall all turnaround time is critical to the ever ongoing maintanence process; it used to be 10min a few years ago, then 20min, now it is approaching 30min again.) 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] Small repository accident
On 02/24/2012 09:01 AM, Florian Haftmann wrote: Accidentally I have pushed something into the main repository which was still supposed to be tested. PLEASE IGNORE HEAD REVISION 0bd7c16a4200 and continue with the other head. Sorry for this, Florian I was close to this mistake myself a couple of times already. It is the "evil" -f option with is now standard when pushing to the testboard -- accidently pushing to the public repository (with -f) is then done without checking as well. Isn't there a easy way to allow pushing to the testboard without writing "-f" but still allowing to create new heads? Then we would never use the -f option and cannot get into this trouble. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On 02/18/2012 10:18 AM, Florian Haftmann wrote: How much relative time do the quickcheck examples in HOL-ex take? According to my feeling time could be high to separate these into a separate session, to facilitate maintenance. I separated the Quickcheck-Examples from HOL-ex into an own session (cf. http://isabelle.in.tum.de/repos/isabelle/rev/f462e49eaf11) The latest performance numbers do not show that the run time reduced, so either there is really another bottleneck or my own change has not had any effect on the measurements yet? (cf. http://isabelle.in.tum.de/devel/stats/at-poly/HOL-ex.png) Maybe we could also get performance measurements for the new session? I hope it facilitates maintenance nevertheless. Although if Quickcheck fails (or does not terminate) after some changes, this usually indicates that there is some flaw in the code generation setup. If Library-Codegenerator-Test works, you only know that you get source code that compiles correctly. With the Quickcheck-Examples session, you know that the source code also runs correctly. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] SML makeall fails
Hi all, for three weeks, SML-makeall is continuously failing with the following error message: [/tmp/mira/workbench/15468-139692104476416/Isabelle/heaps/smlnj_x86-linux/HOL-Proofs] Error 152 [/tmp/mira/workbench/15468-139692104476416/Isabelle/heaps/smlnj_x86-linux/log/HOL-Metis_Examples.gz] Error 152 [/tmp/mira/workbench/15468-139692104476416/Isabelle/heaps/smlnj_x86-linux/HOL-IMP] Error 152 The error occured the first time on changeset 6d2af424d0f8 (cf. http://isabelle.in.tum.de/reports/Isabelle/rev/6d2af424d0f8) and SML-makeall still succeeded on fd21bbcbe61b. In the time between those changesets, mainly three developers have been doing some changes. We should look why the errors occur. Maybe we have to adjust the timeouts for these sessions. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck Examples
On 02/18/2012 10:18 AM, Florian Haftmann wrote: How much relative time do the quickcheck examples in HOL-ex take? According to my feeling time could be high to separate these into a separate session, to facilitate maintenance. Are there any voices pro or contra? IMHO the overhead when figuring out (frequently occurring) non-termination problems in HOL-ex is not tolerable at the moment, so a fat cure would be reasonable. I guess there are no voices at all. If you have strong feelings for yet another session, I can go ahead and split the theories. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Some missing setup for function package in combination with Option-type
Just two comments: First, the discussion about this should be on the isabelle mailing list, not the isabelle developer's mailing list. There has been a discussion just a few days ago that the developer's mailing list is limited to arbitrary repository versions and the related development process, including administrative things like isatest, mira etc. Second, the AFP is a perfect place to also submit small library developments. The List-Index theory is such an example. So, the Option monad could be just turned into a small AFP entry. Lukas On 02/17/2012 12:13 PM, Christian Sternagel wrote: In this respect, maybe the whole file http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/10e7033da765/IsaFoR/Option_Monad.thy is of interest (which includes this cong rule already for some time). If I remember correctly there was no Option.map when we wrote this. Anyways, this could be (at least partly) merged into Option.thy. cheers chris On 02/17/2012 07:59 PM, René Thiemann wrote: Dear all, recently, I stumbled upon the problem, that there is no proper fundef-cong rule for map on Option-types. I added it manually to our developedment, but perhaps this should be integrated in Option.thy lemma option_map_cong[fundef_cong]: "xs = ys \ \\ x. ys = Some x \ f x = g x\ \ Option.map f xs = Option.map g ys" by (cases ys, auto) Cheers, René ___ 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] Regression Test Server lxbroy10 broke down (again)
Hi all, The server lxbroy10 in Munich broke down last night. Our technical support group is trying its best to get it running again. Even if it is up running again, we might have some interruption the next days while they continue to replace some components. For the time, I started a mira daemon with bisect(Isabelle_makeall) on lxbroy6 for the main repository and bisect(Isabelle_makeall) on lxbroy5 for the testboard. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Regain AFP sanity
On 01/11/2012 09:29 PM, Alexander Krauss wrote: The real problem is in fact JinjaThreads. AFAIK, the only machine at TUM where it can still build (in principle) is lxbroy10, but as Lukas pointed out there are still some failures, cf. http://isabelle.in.tum.de/reports/Isabelle/report/628b2a4bd3f94f478b929b72f811c5af. I hope that we can get further data on whether this is a repeatable problem in the next days. NB: JinjaThreads has been failing in the mira testing of the configuration AFP-big since the beginning of testing on lxbroy10. Up to now, we don't know which system configurations is actually causing this failure. But nobody has spent much time to investigate this sofar. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle test failures
I bisected the failure further on my local machine and it turns out it is related to the changeset changeset: 46143:463b594e186a user:wenzelm date:Fri Jan 06 20:18:49 2012 +0100 summary: refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x"; Lukas On 01/11/2012 09:16 AM, Lukas Bulwahn wrote: Hi all, the latest failures of the isabelle test of the form: /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX: Conflicting definitions for `ad' Bound at: /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX-XX /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX-XX In a case alternative causing quickcheck to fail in ex/Tree23.thy is not related to any modifications in quickcheck, but is probably related to some recent changes in the code generator or some setup on macbroy21. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] isabelle test failures
Hi all, the latest failures of the isabelle test of the form: /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX: Conflicting definitions for `ad' Bound at: /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX-XX /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs::XX-XX In a case alternative causing quickcheck to fail in ex/Tree23.thy is not related to any modifications in quickcheck, but is probably related to some recent changes in the code generator or some setup on macbroy21. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck_Exhaustive.unknown
On 12/09/2011 04:41 PM, Florian Haftmann wrote: Unfortunately, the find_theorems command is quite ignorant to any means to hide facts: Facts that have been hidden, can be found. Note that with »hide« you do *not* hide the artefacts, but their name access. The artefacts are still there. You can still argue that anyway find_theorems etc. should ignore everything which cannot by access by name through the name space. I was expecting that *names* hidden with hide_fact do not effect find_theorems -- even though it is quite arguably why the artefacts should be found after that operation. But I am surprised that the Binding.conceal in ML does not have any effect either. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck_Exhaustive.unknown
On 11/30/2011 03:17 PM, Tobias Nipkow wrote: Am 30/11/2011 12:27, schrieb Makarius: This concerns Isabelle/3d6ee9c7d7ef: Adding a global constant Quickcheck_Exhaustive.unknown with rather generic notation "?" to main HOL is a bit dangerous. The name "unknown" is also a candidate for "hide_const (open)". I would like to emphasize this. Local names (i.e. those that the clients of a package or theory do not need to know) should stay local, i.e. should be hidden at the end. This is particularly important if the name is something generic like "Times" or "unknown" that other people may want to use, too, w/o suffering from long names. Quickcheck is particularly generous in what it exports... I looked into this issue this afternoon. First of all, I agree, Quickcheck is particularly generous defining constants: All of its infrastructure must exist in the logic, as it relies on the code generator. The existing hide_const declarations already were hiding all constants in Quickcheck. Changeset 5616fbda86e6 now also hides all definitional theorems. So even the names of theorems are now hidden. Unfortunately, the find_theorems command is quite ignorant to any means to hide facts: Facts that have been hidden, can be found. And also facts that were properly concealed in the ML sources are found. This surprises me as the authors of "find_theorems" seem to be expecting that they are filtering them out, cf. line 524 in find_theorems.ML (changeset e832acb88f43). Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient and typedef
On 12/08/2011 02:35 PM, Florian Haftmann wrote:
Dear all,
since my post on quotient and partiality created some confusion, I want
to cast some light on it from a more direct perspective.
Just a few short comments from my side:
Concerning »typedef«, we currently have two conflicting issues:
a) From a foundational perspective, we want to leave »typedef« untouched
»as it is«
b) Recently, »typedef« in userspace became more popular (again), and
there a some awkward things about it:
* archaic naming, which ignores contemporary namespace conventions
* sets in the specification, which is particularly silly if predicates
already exist (e.g. xs \ {xs. distinct xs} ==> ...)
* technical and difficult-to-remember syntax (do you know by heart in
which order the two morphism symbols have to be written? where to place
an infix syntax, or maybe even a syntax for the morphism symbols? and
that (open) actually denotes that no characteristic set is defined)?
* _.eqI and _.eq_iff, theorems nowadays considered fundamental (cf.
Library/Dlist.thy et al.), are not proved automatically
* desire to automagically register certain type properties (e.g. for the
emerging lifting machinery)
* (maybe you can add more)
I do agree that there is always some confusion when using typedef, but
to some extent, this is simply caused by the fact that we do not define
new types on a daily basis right now.
I also noticed that I sometimes just use a datatype with one constructor
because datatype does provide a few lemmas and I know datatype's syntax
better than typedef's.
None of the b) issues is pressing on its own, but in summary I consider
them critical enough to call for a solution.
My idea then is the following:
1) Leave »typedef« untouched, as (internal) foundational mechanism, for
bootstrap reasons (datatypes prod, sum, nat), and whenever a user thinks
she needs it.
2) Provide a more convenient user-interface for user-space »typedefs«
Now, if »quotient« »as it is« can cover every typedef specification, a
reasonable answer would be to establish »quotient« as the canonical
user-interface for non-datatype type specifications, even for cases like
dlist where there is no non-trivial quotient, and resolve all those b)
issues on the quotient level.
To show that the quotient_type and its friends (quotient_definition, the
lifting method) is useful, Cezary already provided examples of theories
where manual quotient definitions and lemmas were replaced by
definitions and lemmas of the quotient package, e.g., the construction
of the integers.
In my opinion, one part of making the quotient package more visible is
to continue to extend these examples to the point, where we can simply
replace the manual quotient definitions and lifting (in the main images)
by the automatic ones.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Quickcheck
Quickcheck returns variable assignments as counterexamples, which allows to reveal the underspecification of functions under test. For example, refuting "hd xs = x", it presents the variable assignment xs = [] and x = a1 as a counterexample, assuming that any property is false whenever "hd []" occurs in it. These counterexample are marked as potentially spurious, as Quickcheck also returns "xs = []" as a counterexample to the obvious theorem "hd xs = hd xs". After finding a potentially spurious counterexample, Quickcheck continues searching for genuine ones. By default, Quickcheck shows potentially spurious and genuine counterexamples. The option "genuine_only" sets quickcheck to only show genuine counterexamples. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Two simple beginners question
Hello Rene,
On 12/02/2011 03:04 PM, René Thiemann wrote:
Dear all,
I'm currently trying to develop a package for automatic generation of linear
orders for datatypes.
I have already defined some functions which generate the corresponding
equations which encode the linear order.
Now the first question I have is how to store these functions:
- when registering the equations via the function package
(Function.add_function) I essentially have
a local theory transformer of type "lthy -> lthy"
- afterwards, I would like to store the newly created constant of the function
symbol and some other data
in some global store so
that I can reuse it later in other generated orders. Here, I currently use
structure Ordering_Data = Theory_Data( type T = ...)
with the update function Ordering_Data.map (Symtab.update ...)
which is essentially a theory transformer of type "thy -> thy"
- how is it now possible to combine these transformers into one method foo,
such that either
setup {* foo "my_datatype" *} or local_setup {* foo "my_datatype" *}
can both register the function via the function package, and also store all
informations in
the Ordering_Data store.
To be more precise: Is there a way to convert a function (lthy -> lthy) into a
function (thy -> thy)
or vice versa?
It is best practice to make your data storage local, i.e., to a
Generic_Data functor.
Then update the generic data storage with Local_Theory.declaration.
Looking in the sources for the usage of Local_Theory.declaration should
give you a rough pattern, how to employ this function.
The second is a rather simple ML question:
- Is it possible to conveniently update single fields in a record as in OCaml?
E.g., val r1 = {a = 5, b = "foo", c = ..} and many fields
val r2 = '' r1 where only b is changed to "bar" ''
(in OCaml: val r2 = {r1 with b = "bar"})
To my knowledge, there is no convenient update functions for record in
ML provided automatically.
Therefore, many developers just define the ones of interest with some
boiler-plate code.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quickcheck_Exhaustive.unknown
On 11/30/2011 01:14 PM, Makarius wrote:
On Wed, 30 Nov 2011, Makarius wrote:
This concerns Isabelle/3d6ee9c7d7ef:
Adding a global constant Quickcheck_Exhaustive.unknown with rather
generic notation "?" to main HOL is a bit dangerous. The name
"unknown" is also a candidate for "hide_const (open)".
It appears to be used only for output anyway, so the syntax can be
easily attached to the local context before printing.
There are more ways to do it, if slightly different functionality is
required. E.g. see the more advanced Proof_Syntax.proof_syntax or
Nitpick_Model.add_wacky_syntax, although this is heavy gear.
Yet another possibility:
axiomatization unknown :: 'a
notation (output) unknown ("?")
Here 'axiomatization' prevents later definition of that unknown thing.
The output notation prevents pollution of global input grammar.
Changeset 3b7c35a08723 follows your suggestion. Thanks for these hints.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient example with partiality?
On 11/29/2011 06:21 AM, Cezary Kaliszyk wrote: When developing the quotient package we included the infrastructure for defining quotient types with partial equivalence relations, however since one of the main uses was supposed to be nominal (where its always reflexive) we did not test the partial functionality too much. The idea of using the quotient package with partial equivalence relations is that two changes need to be done: First if the user specifies 'partial:' in the quotient_type definition, the obligation to prove changes from 'equivp' to 'part_equivp'. Which is simpler, but then less lifting can be done automatically (to be more precise, some of the theorems that allow for automatic regularization do hold only for reflexive equivalence relations). Hi Cezary, could you add this explanation for the partial option to the existing IsarRef documentation of quotient types to make sure that this piece of knowledge is not just archived here? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient example with partiality?
On 11/28/2011 10:41 PM, Makarius wrote:
On Mon, 28 Nov 2011, Lukas Bulwahn wrote:
many recent requests for adjusting the user-space behavior of typedef
would then rather apply to quotient_type.
Also, I do not see the clear advantage how the suggested change would
make the adjustments simpler. I would rather imagine that the
quotient_type command could be assimilated by extending the typedef
command to enable to hook the pre- and post processing of quotient
type into typedef.
This reminds me of datatype interpretation, but it is more like an
example of super package bloat.
The quotient type defines a type with typedef, defines some further
constants, and sets some declarations.
If typedef becomes a super package, all this could be done somewhere in
typedef with some setup.
While explaining this here, I feel more and more that this is not a good
idea to do at all, and also Florian's suggestion becomes very questionable.
Can you explain further what is the purpose of the pre- and post
processing mentioned above? In 5b0b1dc2e40f I've recently seen this,
but did not have time to look more closely so far, and the lines are a
bit too long for quick reading and understanding.
text {* Here is some ML setup that should eventually be incorporated
in the typedef command. *}
local_setup {* fn lthy =>
let
val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
val qty_full_name = @{type_name "set"}
fun qinfo phi = Quotient_Info.transform_quotients phi quotients
in lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Quotient_Info.update_quotients qty_full_name (qinfo
phi)
#> Quotient_Info.update_abs_rep qty_full_name
(Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep =
@{term "member"}}))
end
*}
At first sight this looks like some dummy data item is retrofitted to
typedefs that are not full quotient types. Couldn't the Quotient_Info
lookup do this on the spot as a fall-back? Or is there anything
special with full declarations and morphisms here?
You are right, some dummy data item is retrofitted to typedef that are
not full quotient types.
Eventually, some general parts of the quotient type infrastructure
should also be usable for simple type definitions.
Obviously, it is easy to hook into the quotient type infrastructure with
dummy data to obtain the wished results, that is what 5b0b1dc2e40f does.
Doing it right, separating the general parts from the specific parts for
equivalence relations and quotients correctly, is hard work, which we
addressing
in near future.
The source code above disappears when we understand how the
generalisation looks like, how the data structures must be separated
(making dummy data or lookup with default dummy data obsolete), and how
we present this to the
user on the Isar level.
The current noise in this file will be reduced as we proceed.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Quotient example with partiality?
On 11/28/2011 07:25 PM, Florian Haftmann wrote: Hi all, I'm asking myself the question how one would define rational numbers using the quotient package. The key issue is that the equivalence relation here is partial, ruling out denominators of value zero. In the Isabelle reference manual I can find »partial:« in a syntax diagram but not any concrete example in the distribution. The reason why I ask is that I want to understand if *every* typedef specification can be written as quotient type specification (in a straightforward manner). If yes, quotient_type could replace typedef in user space in general, and many recent requests for adjusting the user-space behavior of typedef would then rather apply to quotient_type. Actually, the quotient package does more than an simple type definition. It also defines some further constants. many recent requests for adjusting the user-space behavior of typedef would then rather apply to quotient_type. Also, I do not see the clear advantage how the suggested change would make the adjustments simpler. I would rather imagine that the quotient_type command could be assimilated by extending the typedef command to enable to hook the pre- and post processing of quotient type into typedef. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP failure in Lam-ml-Normalization
On 11/17/2011 09:33 PM, Alexander Krauss wrote: retesting the same revisions that just worked two days ago, now yields an error, cf. http://isabelle.in.tum.de/reports/Isabelle/rev/6975db7fd6f0. The system configuration (probably of LaTeX) must have changed in past few days. We will have to investigate that further. I don't have the issue on my machine (yet), but maybe this solves it: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/4f0607411284 :-) Alex Thanks, Alex. This resolved this issue, cf. http://isabelle.in.tum.de/reports/Isabelle/report/7e2b88fe3d9e4f99a461d28b37bf373d. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP failure in Lam-ml-Normalization
On 11/17/2011 11:58 AM, Jasmin Christian Blanchette wrote: Hi again, When it comes to the AFP failure, there's a second AFP failure, in JinjaThreads, that's obviously related to the servers' being down yesterday; the Lam-ml-Normalization failure could be due to that, too. Lukas is helping find out. Hi all, retesting the same revisions that just worked two days ago, now yields an error, cf. http://isabelle.in.tum.de/reports/Isabelle/rev/6975db7fd6f0. The system configuration (probably of LaTeX) must have changed in past few days. We will have to investigate that further. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Float
On 11/14/2011 09:35 PM, Florian Haftmann wrote: @Florian: Is it imaginable to add such unsound setup in a way that it does not infect the evaluation oracle by default? Indeed. More on that another time (when I find some time). Florian @Johannes: If you aim at adding another code target for this theory, I can assist with the setup. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL-Mutabelle broken
With changeset aa35c9454a95, HOL-Mutabelle compiles again. Lukas On 11/09/2011 06:16 PM, Makarius wrote: In Isabelle/d17556b9a89b HOL-Mutabelle is broken: HOL-Mutabelle FAILED (see also /Volumes/Macintosh_HD/Users/makarius/.isabelle//heaps/polyml-5.4.2_x86_64-darwin/log/HOL-Mutabelle) *** int list -> term list option * Quickcheck.report option ***Reason: ***Can't unify string * Quickcheck_Common.compile_generator to *** Proof.context -> *** (term * term list) list -> *** int list -> term list option * Quickcheck.report option *** (Incompatible types) *** Error (line 499 of "~~/src/HOL/Mutabelle/mutabelle.ML"): *** Type error in function application. ***Function: *** Quickcheck_Common.test_term *** Exhaustive_Generators.compile_generator_expr *** ctxt' *** : bool -> term * term list -> Quickcheck.result ***Argument: (true, false) : bool * bool ***Reason: Can't unify bool to bool * bool (Incompatible types) *** *** At command "theory" (line 1 of "~~/src/HOL/Mutabelle/MutabelleExtra.thy") Exception- TOPLEVEL_ERROR raised *** ML error I have tried to repair this myself, but failed to understand the 3-4 changesets leading up to that problem -- just too many obscure booleans floating around, and no proper explanations in the changelogs. 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] Merge-Sort Implementation
On 10/27/2011 04:38 PM, Florian Haftmann wrote: Nonetheless, we still have the real-based Library.random from "ML for the working programmer", because without it quickcheck performs really bad. AFAIR this has only been the case for the ancient SML quickcheck, whereas my quickcheck implementation comes with a random generator in HOL based on a cousin in Haskell. If this is true, we could throw away Library.random. Maybe Lukas can comment on this. What Florian mentioned is correct. A closer code inspection tells me: Matrix/Compute_Oracle/am_sml.ML still uses it to get a unique identifier, probably this can be replaced by a more standard serial_string () Slegdehammer uses it to randomly announce information from Geoff Sutcliffe to our users. Mutabelle has another copy of a Random engine for some random-choice function. It is seems feasible to get rid of the Random engine if one can replace these occurrences by something else appropriate. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Fwd: status (AFP)
Hi all, JinjaThreads currently probably fails because of the changeset 6e422d180de8 (http://isabelle.in.tum.de/repos/isabelle/rev/6e422d180de8) *** empty result sequence -- proof command failed *** At command "apply" (line 2941 of "/home/kleing/afp/devel/thys/JinjaThreads/Compiler/JVMJ1.thy") val it = (): unit Exception- TOPLEVEL_ERROR raised *** ML error I could not even inspect the proof state where it fails, as my machine is not able to load the theory. If anyone here has an educated guess how this proof can be fixed, you should try. There are at least two machines, lxbroy10 in Munich, and one in Australia, running regularly that can check these guesses once you push them. Lukas Original Message Subject:status (AFP) Date: Fri, 21 Oct 2011 06:31:55 +1100 From: Gerwin Klein To: undisclosed-recipients:; The status of the following AFP entries changed or remains FAIL: [JinjaThreads] is still on FAIL. Full entry status athttp://afp.sourceforge.net/status.shtml AFP version: development -- hg id a98f0ac6930a Isabelle version: devel -- hg id c4fab1099cd0 Test ended on: lemma, Fri Oct 21 06:31:55 EST 2011. Have a nice day, isatest ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle test failed
The failure is intended to be fixed with changeset 66ba67adafab and was related to changes in 3f1d1ce024cb. Lukas On 10/20/2011 12:19 PM, Makarius wrote: On Thu, 20 Oct 2011, Account Isatest wrote: Test for platform at-poly-test failed. Log file attached. [...] 3:02:39 elapsed time, 3:11:31 cpu time, factor 1.04 Logics HOL FAILED! --- test FAILED --- Thu Oct 20 03:25:34 CEST 2011 --- macbroy21 Again the same failure. Here are the relevant parts of the log: Isabelle version: 3dd426ae6bea Started at Thu Oct 20 00:22:55 CEST 2011 (polyml-5.4.2_x86-linux on macbroy21) Running HOL-Proofs-Extraction ... Linking /tmp/isabelle-isatest24752/Quickcheck_Narrowing893907/isabelle_quickcheck_narrowing ... Linking /tmp/isabelle-isatest24752/Quickcheck_Narrowing893923/isabelle_quickcheck_narrowing ... HOL-Predicate_Compile_Examples FAILED (see also /home/isatest/isabelle-at-poly-test/heaps/polyml-5.4.2_x86-linux/log/HOL-Pre dicate_Compile_Examples) (unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence) -> Proof.context -> Proof.context val put_dseq_result : (unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)) -> Proof.context -> Proof.context val nrandom : int ref val no_higher_order_predicate : string list ref val function_flattening : bool ref val debug : bool ref end *** Error (line 377 of "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"): *** Value or constructor (instantiate_goals) has not been declared in structure Quickcheck *** Error (line 381 of "~~/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML"): *** Value or constructor (collect_results) has not been declared in structure Quickcheck *** This problem might show up now, because I have updated Poly/ML SVN version behind the unofficial "polyml-5.4.2" quoted above. Also note that raw stderr is for system log only, not user messages or side-effect of user command invocation. So "Linking ..." should probably be directed to stdout in the shell script, such that Isabelle_System.bash_output could take care of it via regular writeln. 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] Code generation in Isabelle
Hello all, I am reporting on the continuation to remove the ancient code generator, related to an earlier mail this July. at the moment, we have two code generators in Isabelle: 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML without supporting type classes. Commands to invoke it were code_module and code_library. 2. A generic code generator in Isabelle by Florian Haftmann - extenible to multiple target languages, supporting type classes, basic integration of reflection and abstraction mechanisms Commands to invoke it are export_code, value, code_reflect, and some others. The second subsumes the first, so we intend to remove the first code generator from the next Isabelle distribution if there are not any strong defenders of the ancient code generator. We are getting closer to remove the ancient code generator. In this process, the preprocessing attributes of the code generator code_unfold and code_inline now have the same semantics. Hence, only one has to be kept. At the moment, there are four attributes related to code generation preprocessing, code_unfold and code_inline, code_post and code_unfold_post. Florian and I are not sure if code_inline or code_unfold fit better to the intended behaviour of "rewriting a code equation by some simplifying equation" (unfolding a term by its definition, or inlining the definition). Does anyone have a suggestion? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mira on lxbroy10
On 10/16/2011 10:06 PM, Alexander Krauss wrote: On 10/16/2011 02:53 PM, Florian Haftmann wrote: On lxbroy10, something is utterly wrong: http://isabelle.in.tum.de/testboard/Isabelle/report/89d77033f6eb4dc196c199893871ae6d Is anyone taking care for this? Just tried to fix with Isabelle/efc2e2d80218. Current tests unfortunately still fail, e.g. http://isabelle.in.tum.de/reports/Isabelle/report/93b3825f1b7747b4afc0f1808f90bd18 The reason was not apparently to me after staring at it for ten minutes, so I hope you have time to look at it maybe once more. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] mira on lxbroy10
On 10/16/2011 10:06 PM, Alexander Krauss wrote: On 10/16/2011 02:53 PM, Florian Haftmann wrote: On lxbroy10, something is utterly wrong: http://isabelle.in.tum.de/testboard/Isabelle/report/89d77033f6eb4dc196c199893871ae6d Is anyone taking care for this? Just tried to fix with Isabelle/efc2e2d80218. In general, Lukas and Lars now also feel responsible for the mira installation at TUM, so in general there is no reason to panic :-) We monitor the reports manually, and the functionality of the testing infrastructure (mira daemons) automatically by the chair's monitoring facility. But the Isabelle development testing infrastructure is not a running service for thousands or millions of users, hence our reaction time is moderate (within the next working day, and not within the next few minutes). Unnoticed by others, we restart some daemons around once to twice a week to keep the testing infrastructure running. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/563de86630d9
On 10/13/2011 10:52 AM, Florian Haftmann wrote: Hi Lukas, »removing checking of generated code because it fails on the mira testing infrastructure due to a missing Pure image« – I don't quite understand this. Why exactly is the check failing? Florian The issue can be observed at http://isabelle.in.tum.de/reports/Isabelle/report/5497697969e943bda524c4b01be7d12e Checking that the generated code in the Depth-First-Search AFP entry actually compiles with ML is a minor point anyway, so I did not dig into the details, but removed the check instead. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cs. 3911cf09899a
On 10/03/2011 10:04 PM, Florian Haftmann wrote: If you have strong feelings about this being at the wrong place, you can move it. I have no »feelings«, just an educated guess that sometimes somebody *will* move it, either by necessity or by psychological strain. In an amortized view, you do not save any work by leaving it as it is. Then, we will move it when the time has come to do so. I guess the following AFP problem results from that fundamental change: http://isabelle.in.tum.de/reports/Isabelle/report/11aa8e74cf064dc9bb9c10f72882a9d0 I resolved this two days ago, but the internet connection at the workshop I am attending limits my ability to make changes public immediately. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] cs. 3911cf09899a
On 10/03/2011 04:59 PM, Florian Haftmann wrote:
+text {* Definitions could be moved to Transitive_Closure if they are
of more general use. *}
is there any striking reason *not* to do so in the first place? At a
first glimpse I can't see anything which relates to Enum.thy in those
theorems.
Well, the definition is made because it is not possible to define
recursive functions
inlined in other definitions in Isabelle.
Otherwise, I could have avoided it at all.
In my opinion it is high time to abandone the tradition of such comment
jokes in the HOL theories: if theorems are there, they *will* be used,
or at least it is not at our judgment for whom they are useful. So it
is best to have the theorems where they belong to, unless bootstrap
reasons dictate something else.
The theorems are useful for my development, but I can't judge if they
are useful
in general.
More specifically, adding this definition correctly would also require
to prove many
more basic lemmas, such as introduction and elimination rules.
In this way, I am following a long tradition of tool developers,
defining constants for
their "internal" purposes, which we hope are not picked up by users.
You can find these traditions in almost every tool in the HOL image.
But what you are suggesting is that anything related to some concept
must be in that
specific theory.
But there are obvious counterexamples, such as More_List, and different
Util Theories
that contain specific definitions and lemmas, sofar only used in those
developments.
If you have strong feelings about this being at the wrong place, you can
move it.
+subsection {* An executable card operator on finite types *}
+
+lemma
+ [code]: "card R = length (filter R enum)"
+by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV
Collect_def)
Our current efforts for having 'a set as type constrcutor will turn this
superfluous if not hindering.
I was aware of this aspect when writing this lemma.
If it hinders the efforts, it might actually be because the predicate
and set distinction has consequences,
we have overlooked sofar.
The definition of card(inality) is clearly related to sets.
But will there also exist a definition of the cardinality of a predicate?
For lemmas about the tranclp predicate, one needs the number of values
for which a relation is true (the cardinality).
So, what's the opinion on this?
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Open Issues with JinjaThreads entry
Hello all, the traditional isatest's AFP-Test did not report any failures the last few days, but the emerging testboard infrastructure mentions failures over the last few versions, and the current tips 76aec35b4898934df700ee54ce4d8fb7b99b0388:AFP,fa3715b35370fd27bc9e6bd03fad4a34b0724af3:Isabelle still seem to be broken. For people involved in this issue, here is a more detailed report: http://isabelle.in.tum.de/reports/Isabelle/report/37c2d104871b443f8b6dbd0a8b8b0314 Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS -> Redundant lemmas
On 09/22/2011 11:36 AM, Peter Lammich wrote: Perhaps we should start using a standardized process for phasing out legacy theorems, like moving them into a separate theory file "Legacy.thy" that would not be imported by default, and would be cleared out after each release. When upgrading Isabelle, users could import Legacy.thy as needed to get their theories working, and then work gradually to eliminate the dependencies on it. What do you think? If one tries to follow Brian's idea, even with the Legacy.thy, there is still no guarantees that by importing the theory, everything works as with the release before. For some incompatible changes, retaining compatibility within another theory is larger than the change itself. But for the special case of phasing out legacy theorems, it might work, but then I would only restrict this Legacy theory to selected theories (maybe everything within HOL-Plain or even less). In Java, there is a "deprecated" flag for such issues. Isabelle could then issue a warning whenever using a deprecated lemma --- like the "legacy"-warnings it already issues when using some deprecated features (recdef, etc.) You are assuming that you could flag theorems, and all tools know what these flags should actually mean, and if they use them. That's technically quite difficult to achieve. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Testboard reset: Old Testboard changesets are removed
Hello all, Lars and I have taken over the maintenance of the reports and testboard from Alex yesterday. Today, due to some storage issues, we did not learn early enough about, the testboard repository changed into an inconsistent state. I reset the testboard repository to start with a clean clone from the development repository and now everything should work again. If anyone is eager to restore the old testboard's changesets, we are happy for any assistance, otherwise we will discard them within the next week, if no one objects. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
Thanks. I've set the JinjaThreads test to run every day now, at least until the release. In Munich, we now also use our number cruncher lxbroy10 to run the large (non-frequently tested) AFP sessions within the new testing infrastructure. This should give us some more light on failures of these AFP theories in the future. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
On 09/19/2011 01:56 PM, René Thiemann wrote:
Dear all,
There are still some improvements to the Haskell serializer and the code
generator I would like to get into the release.
After some discussions with Florian, the remaining changesets are about ready
and final, so I can probably commit them till this Wednesday.
Afterwards, the code generator is probably best checked against the two largest
executable formalisations (JinjaThreads and CeTA) -- I will try to get the
developers to re-run these with a current repository version or the first
pre-release version.
When reading this post (and since we will port to the new distribution in any
way), I started to adapt our library to the upcoming version where I used the
bundle http://www4.in.tum.de/~wenzelm/test/Isabelle_11-Sep-2011/download.html
After some first adaptations I got stuck when at the first place where we use
partial_function. It seems that the partial_function package is broken if
polymorphic types are used. (which was not the case in Isabelle2011)
partial_function(option) foo :: "nat list \ unit option" where "foo x =
foo x"
works, but
partial_function(option) foo :: "'a list \ unit option" where "foo x =
foo x"
yields the following error message.
*** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type conflict
*** ?F :: (?'a2 list \ unit option) \ ?'a2 list
\ unit option
*** \foo. foo :: ('a list \ unit option) \ 'a
list \ unit option
*** At command "partial_function" (line 216 of
"/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy")
or if I output sorts
*** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type conflict
*** ?F\(?'a2\type list \ unit option) \ ?'a2\type list
\ unit option :: (?'a2\type list \ unit option) \ ?'a2\type
list \ unit option
*** \foo\'a\type list \ unit option. foo :: ('a\type list
\ unit option) \ 'a\type list \ unit option
*** At command "partial_function" (line 216 of
"/Users/rene/devel/rewriting/IsaFoR/Loops_Impl.thy")
I think this is a triviality since it looks to me that one just has to replace
?a2 by 'a,
but I do not know where to fix it.
After that, I'm happy to test any further version, also repository snapshots.
Alex seems to have fixed this issue with changeset 8b74cfea913a -- so,
if you can get hold on any version >= 8b74cfea913a, you can report if
there are further unresolved issues.
The mentioned changes of the code generator are also already in the
repository.
Lukas
Cheers,
René
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Towards release
Hello all, Are there any further things in the pipeline? In the final phase one needs a bit more organization than the "push first, fix later" cycle that occasionally happens outside this special season. There are still some improvements to the Haskell serializer and the code generator I would like to get into the release. After some discussions with Florian, the remaining changesets are about ready and final, so I can probably commit them till this Wednesday. Afterwards, the code generator is probably best checked against the two largest executable formalisations (JinjaThreads and CeTA) -- I will try to get the developers to re-run these with a current repository version or the first pre-release version. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
