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
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] 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 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 vacation and not forseeing
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] 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 Haftmannflorian.haftm...@informatik.tu-muenchen.de 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
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] 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
[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
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 Purethy files 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] 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] 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] 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
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] 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
[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
[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
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] 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] 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] 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: ... proof 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
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
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
[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] 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 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] 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] 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 Nipkownip...@in.tum.de 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] 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
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. 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 \Longrightarrow \lbrakk\And x. ys = Some x \Longrightarrow f x = g x\rbrakk \Longrightarrow 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] 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] 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] 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 \in {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] 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/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/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] 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] 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 kle...@ertos.nicta.com.au 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] 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] 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] 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 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
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
[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] 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 \Rightarrow unit option where foo x =
foo x
works, but
partial_function(option) foo :: 'a list \Rightarrow 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 \Rightarrow unit option) \Rightarrow ?'a2 list
\Rightarrow unit option
*** \lambdafoo. foo :: ('a list \Rightarrow unit option) \Rightarrow 'a
list \Rightarrow 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\Colon(?'a2\Colontype list \Rightarrow unit option) \Rightarrow ?'a2\Colontype list
\Rightarrow unit option :: (?'a2\Colontype list \Rightarrow unit option) \Rightarrow ?'a2\Colontype
list \Rightarrow unit option
*** \lambdafoo\Colon'a\Colontype list \Rightarrow unit option. foo :: ('a\Colontype list
\Rightarrow unit option) \Rightarrow 'a\Colontype list \Rightarrow 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
Re: [isabelle-dev] NEWS / CONTRIBUTORS
On 09/12/2011 07:29 PM, Florian Haftmann wrote: Hi Lukas, the rename AssocList ~ AList_Impl should sound AssocList ~ AList Nota bene: T.thy – theory as intended to be used by other theoreis T_Impl.thy – implementation for abstract type Since ALists are not abstract, there is no AList_Impl.thy, but cf. RBT_Impl.thy. The rename AssocList ~ AList will be fruitful in the middle run: generic operations with popular names should be qualified, and AssocList.update will not do. The data structure library theories then can orient more and more towards the Isabelle/ML library (fragments of this intension already showing up in More_List.thy). Florian The rename AssocList to AList_Impl was actually already glimpsing into the future, where there will exist an abstract AList, as our brave users have already done this in the AFP-Collections framework. I now followed your suggestion, but in the future, this will be revised once again, until the Isabelle/ML library and the HOL/Library theories coincide. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Option raised errors hides other error failures
On 09/09/2011 02:52 PM, Makarius wrote: On Fri, 9 Sep 2011, Lukas Bulwahn wrote: In my concrete case: When running the compilation within the make command, I get: *** exception Option raised Exception- TOPLEVEL_ERROR raised *** ML error Whereas running it interactively in PG: *** exception Match raised *** At command code_reflect The Match raised is the real reason for the exception in my case, and the one I was expecting. The Option raised exception seems to caused somehow as a consequence of the previous exception within the non-interactive run. There can be a variety reasons for that. Historically, the tty loop (that is still used in PG) always had slightly different ideas about command execution than the regular batch mode. Since a couple of years, I am trying to unify this in the new interactive document mode, but we are not there yet. (At the moment the latter is just a third variant. What does your example do in Isabelle/jEdit?) Another difference is sequential vs. parallel execution. Passing things through the future farm can influence exception behaviour in certain ways, although ML user code can be written to be well-defined in this respect. In the concrete situation, above one needs to isolate the true reason for the unexpected non-determinism. Either by bisection over the history (induction over the construction of the sources) or by investigating the current version at runtime, with Toplevel.debug, exception_trace etc. in the usual way (this can be like reading tea leaves). I am myself curious to see what is the cause of this particular breakdown. Makarius I investigated the case a little bit more. It does occur with PolyML 5.2.1, but not with PolyML 5.3.0. Moving to PolyML 5.3.0 solves the issue for me, but there might be some other long-term users out there, still enjoying the 5.2.1 version. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Option raised errors hides other error failures
Hello all, lately, I have noticed that the exception handling within the non-interactive execution has changed, disguising the true origin of exceptions. In my concrete case: When running the compilation within the make command, I get: *** exception Option raised Exception- TOPLEVEL_ERROR raised *** ML error Whereas running it interactively in PG: *** exception Match raised *** At command code_reflect The Match raised is the real reason for the exception in my case, and the one I was expecting. The Option raised exception seems to caused somehow as a consequence of the previous exception within the non-interactive run. Is this an intended behaviour? If so, it might be good to know for other developers, not to be mislead by the error message. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] unbound Code.add_type_cmd
Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue. Lukas On 09/02/2011 11:40 AM, Lukas Bulwahn wrote: The reason that this issue has just recently become apparent, is due to changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in replacing (Stefan Berghofer's) SML code generator invocations by generic code generator invocations to enable the long-term removal of the SML code generator. I agree, Florian knows probably best how to resolve this issue easy and clean. In the long run, we are planning to get rid of Executable_Set and add_type_cmd anyway by providing data refinement within the logic (and/or the current efforts towards a own set type). Lukas On 08/29/2011 04:37 PM, Makarius wrote: For quite some time isatest produces the following error with SML/NJ: Loading theory Executable_Set *** Error in /mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/Executable_Set.thy *** instream:2.3-2.20 Error: unbound variable or constructor: add_type_cmd in path Code.add_type_cmd *** At command setup (line 25 of /mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/E This is because SML/NJ does not have managed ML names spaces within the theory context as Poly/ML. So any overriding of structure Code on the toplevel stays persistent. The conflict is caused by the code generator itself: it provides a static structure Code (in ~~/src/Pure/Isar/code.ML), and uses the same name to wrap up generated code in certain situations. Grepping for Code in the sources reveals some such places. Florian probably knows best how to avoid this overlap. 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] unbound Code.add_type_cmd
The reason that this issue has just recently become apparent, is due to changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in replacing (Stefan Berghofer's) SML code generator invocations by generic code generator invocations to enable the long-term removal of the SML code generator. I agree, Florian knows probably best how to resolve this issue easy and clean. In the long run, we are planning to get rid of Executable_Set and add_type_cmd anyway by providing data refinement within the logic (and/or the current efforts towards a own set type). Lukas On 08/29/2011 04:37 PM, Makarius wrote: For quite some time isatest produces the following error with SML/NJ: Loading theory Executable_Set *** Error in /mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/Executable_Set.thy *** instream:2.3-2.20 Error: unbound variable or constructor: add_type_cmd in path Code.add_type_cmd *** At command setup (line 25 of /mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/E This is because SML/NJ does not have managed ML names spaces within the theory context as Poly/ML. So any overriding of structure Code on the toplevel stays persistent. The conflict is caused by the code generator itself: it provides a static structure Code (in ~~/src/Pure/Isar/code.ML), and uses the same name to wrap up generated code in certain situations. Grepping for Code in the sources reveals some such places. Florian probably knows best how to avoid this overlap. 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] (Re-)introducing set as a type constructor rather than as mere abbreviation
Stefan Berghofer wrote:
Alexander Krauss wrote:
In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type ((expr * state) * (expr * state))
set, and turning it into a 4-ary predicate (expr = state = expr =
state = bool) would cause problems with either version of the
transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy
uses a binary predicate over pairs, which requires massaging the
induction rule using [split_format (complete)]].
Hi all,
let me take the opportunity to advertise a useful feature of the induct
method that avoids such manual massaging of induction rules. For example,
the command
proof(induct rule: small_step_induct)
in HOL/IMP/Types.thy can be replaced by
proof(induct (c,s) (c',s') arbitrary: c s c' s' rule: small_step.induct)
which allows the standard induction rule small_step.induct to be used instead
of the small_step_induct rule produced using split_format, which is a bit of
a hack anyway. The above is a shorthand for
proof(induct x==(c,s) y==(c',s') arbitrary: c s c' s' rule:
small_step.induct)
Since revision b0aaec87751c (Jan 2010), the equational constraints arising from
such invocations of induct are solved automatically using injectivity /
distinctness
rules for datatypes, so the rest of the proof script works as if the custom-made
induction rule had been applied.
Hi Stefan,
In most cases, the advertised feature of the induct method does the job
to avoid manual massaging of the induction rule, as you outlined in your
mail. But in certain cases, the features of the induct method do not
supersede the massaging, e.g. with split_format.
Consider the following example:
inductive R :: ('a * 'b) = ('a * 'b) = bool
where
R x y == R y z == R x z
lemma R (a, b) (c, d) == True
proof (induct (a, b) (c, d) rule: R.induct)
oops
lemmas R_induct = R.induct[split_format (complete)]
lemma
R (a, b) (c, d) == True
proof (induct rule: R_induct)
oops
In the first case, you obtain a free variable y of pair type, and
usually it requires to obtain y's components within the proof step,
there is no possibility to get this splitting with the induct method
right now. Using split_format enables this splitting, as you can see in
the second example. This drawback actually stopped us integrating the
method for doing more automatic rule inductions, which we discussed
offline last Christmas.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
On 08/19/2011 07:39 AM, Tobias Nipkow wrote:
Am 19/08/2011 00:00, schrieb Stefan Berghofer:
Alexander Krauss wrote:
I want to emphasize that the limitation of the code generator mentioned
here not only applies to sets-as-predicates but also to
maps-as-functions and other abstract types that are often specified in
terms of functions (finite maps, almost constant maps, etc.). Thus,
having good old 'a set back is does not fully solve this problem as a
whole, just one (important) instance of it.
My view on this whole topic is outlined in the report I recently sent
around (http://www4.in.tum.de/~krauss/papers/refinement.pdf, not updated
since last time). In the long run, I would prefer to see flexible
transport machinery to move stuff between isomorphic types.
Hi Alex,
thanks for your excellent report, I fully agree with this view. There is
often a tradeoff between executability and conciseness / abstractness of
specifications, so I don't think it is a good idea to tweak the logic in
such a way that it is more suitable for code generation.
Having a separate type set is more not less abstract. Just like LISP is
not more abstract than ML. It allows us to regain a few important things
we lost. Sets as predicates are indeed more concise (you don't need {x.
P x} and %x. x : S), but this is just a matter of degree, not a complete
loss of some feature.
If we could freely mix sets and predicates as we had hoped, it would be
different. But proof support is lacking. Not just in Isabelle/HOL, but
Michael Norrish tells me that in HOL4 it is also better not to mix sets
and predicates if you want proof automation.
For example,
HOL/MicroJava/DFA/Kildall.thy uses the SOME operator to select an element
from the worklist, which is highly non-executable but more abstract, since
one does not have to commit to a particular strategy for selecting the element.
This is a misunderstanding. The SOME operator *does* commit to a
particular strategy, but we do not know which one. Which means that we
can never prove it equivalent to any strategy. SOME is both abstract and
concrete in a way that defeats implementation.
Andreas Lochbihler and I elaborate on this topic in our recent paper for
the ITP, cf.
http://pp.info.uni-karlsruhe.de/publication.php?id=lochbihler11itp (page 14)
We present some solutions for code generation when using underspecification.
Put simply, the message is: Do not use Hilbert's choice if you want to
obtain an executable specification.
Of course, handling underspecification is an orthogonal issue to the
subject of this thread.
Lukas
Tobias
Greetings,
Stefan
___
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] Code generation in Isabelle
On 07/25/2011 10:25 AM, Makarius wrote: On Sun, 24 Jul 2011, Alexander Krauss wrote: Anyway, the standard procedure for removal of old stuff is to start marking it as old or legacy in the NEWS, and emitting suitable legacy_warnings. I will follow that standard procedure, once all occurrences of the old code generator invocations are replaced. Put in legacy warnings already now, as they will alert users who accidentially type the wrong commands (remember our experience with the methods evaluation vs. eval last week). You don't have to wait with this until all else is resolved. Yes, waiting until certain things are done tends to pile up a lot of unfinished things. The system is grown (and reduced) from the bottom up, one well-defined step after another. The situation all else is resolved is only ever achieved asymptotically. Legacy warnings are in place; After the next release, the SML code generator will disappear from the HOL image. Lukas Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Code generation in Isabelle
On 07/24/2011 04:57 PM, Makarius wrote: On Thu, 21 Jul 2011, Lukas Bulwahn wrote: 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. I have asked this question several years ago already, but there were a few reasons not to delete it immediately, which I have forgotten (or not fully understood in the first place). As you have asked this question several years ago, it seems like an effort that is worthwhile to be continued. Several years ago, there still were some open issues, execution of inductive predicates, executing partial functions, program extraction, which now should all be resolved -- or only minor issues remain, that could now be fixed easily. Some months ago I have renovated some really old HOL reference manual material, and moved the new version to the isar-ref. This has included the code generator, see section 10.15.2 in isar-ref of Isabelle/521de6ab277a. Apart from repainting the walls and renewing the wallpapers just before demolition, I've also observed that the old code generator is still in use in several places: some applications by Stefan Berghofer (HOL-Proofs/Lambda and Extraction, AFP/POPLmark-deBruijn), and MicroJava and its clones/descendants in AFP. I will look at these applications, and can probably replace them by new equivalent operations with the new code generator. Anyway, the standard procedure for removal of old stuff is to start marking it as old or legacy in the NEWS, and emitting suitable legacy_warnings. This can also mean to move the source modules to another place, like src/HOL/Library/Old_Codegen.thy in this situation. After 1 or 2 full release cycles the material is then removed altogether. Things that have been there for such a long time cannot be removed abruptly, without causing damage or confusion somewhere. I will follow that standard procedure, once all occurrences of the old code generator invocations are replaced. Aside: On page 232 of the above-mentioned manual there is an example about const_code wfrec. The same is still used here in MicroJava: http://isabelle.in.tum.de/repos/isabelle/annotate/eee4fa79398f/src/HOL/MicroJava/J/TypeRel.thy#l100 The source says Code generator setup (FIXME!). The changelog says: no consts_code for wfrec, as it violates the code generation = equational reasoning principle (before it was in src/HOL/Wellfounded.thy). Does that mean there is something utterly wrong with MicroJava? I will look into this issue and can report here, in the changelog, or in the NEWS about its solution. Lukas Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Countable instantiation addition
On 07/22/2011 09:36 AM, Alexander Krauss wrote: datatype foo = deriving countable, finite, Tobias also mentioned set_of, map_of, etc. But since these aren't class instantiations (we have no constructor classes such as functor), we end up with the good old generic datatype interpretation (roughly: datatype - theory - theory). So it seems like we simply want named datatype interpretations that are explicitly invoked via deriving (stretching the original Haskell notion quite a bit...) Yes, this was my first goal for the deriving project, creating a nice user interface and providing a implementation guide for datatype interpretations, and automatic type class instantiations, which would end up as recipe in the Isabelle Cookbook. A second goal was to automatically derive the interpretation by asking the user to give the definitions for some examples (as this can also be done in Haskell). Of course, the student would have to have a strong ML background and must learn a lot about data types. Therefore, I wrote the project idea down, even if such a prospective student might never exist. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Countable instantiation addition
On 07/22/2011 10:44 AM, Lukas Bulwahn wrote: On 07/22/2011 09:36 AM, Alexander Krauss wrote: datatype foo = deriving countable, finite, Tobias also mentioned set_of, map_of, etc. But since these aren't class instantiations (we have no constructor classes such as functor), we end up with the good old generic datatype interpretation (roughly: datatype - theory - theory). So it seems like we simply want named datatype interpretations that are explicitly invoked via deriving (stretching the original Haskell notion quite a bit...) Yes, this was my first goal for the deriving project, creating a nice user interface and providing a implementation guide for datatype interpretations, and automatic type class instantiations, which would end up as recipe in the Isabelle Cookbook. A second goal was to automatically derive the interpretation by asking the user to give the definitions for some examples (as this can also be done in Haskell). Of course, the student would have to have a strong ML background and must learn a lot about data types. Therefore, I wrote the project idea down, even if such a prospective student might never exist. I forgot to mention that the deriving project I was talking about was one of the project ideas for this year's Google Summer of Code, which was not chosen to be completed. 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
[isabelle-dev] Code generation in Isabelle
Hello all, 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. Any thoughts? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing HOL/Import
On 07/20/2011 09:34 PM, Florian Haftmann wrote: Dear all, with Cezary's guidance, I set up mira configurations for building the proofs bundle from the HOL Light repository and for running the HOL-Generate-HOLLight with that bundle, cf. http://isabelle.in.tum.de/reports/Isabelle/report/ed3813d5499d44f6be414a5f051e85f3 for the first successful run. I experienced some fairly reproducible segmentation faults on some machines, but lxbroy5-9 seem to work. This is still prior to Cezary's major cleanup in 6ca79a354c51, so there is hope for improvements here. these are good news, thanks for the excellent work that is going on! A humble question: is there any chance that also the HOL4 import can be covered? As we discussed at lunch in Munich, we have an expert on HOL4, Thomas Tuerk, who might take that opportunity. Lukas 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
[isabelle-dev] Bad binding warnings
Hi, Working with the development version, I have been noticing warnings ... Bad binding: Is there now a stricter guideline using or creating bindings that Isabelle's developers should follow? Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Evaluation of floor and ceiling
On 07/08/2011 03:13 AM, Brian Huffman wrote: I wrote to Florian about this exact issue back in February 2010. Florian's recommended solution at the time was to add a new subclass of archimedean_field that fixes the floor function and assumes a correctness property about it. This solution is really easy to implement (see attached diff). If people think this is a reasonable design, then I'll let someone else go ahead and test and commit the patch. I think it is reasonable, so I added your changeset and set up the code generator and added a simple test case for quickcheck showing that we can evaluate floor and ceiling now. These preliminary changesets can be inspected under http://isabelle.in.tum.de/testboard/Isabelle, and I will push them into the mainstream repository, once the tests ran through. @Brian: Thanks for your effort. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Feedback from a Isabelle tutorial
Hello all, this week, we, Johannes Hoelzl and me, gave a two-and-half-hour tutorial to Isabelle at a workshop meeting of PhD students in computer science in Dagstuhl (cf. http://www.model.in.tum.de/um/vernetzungstreffen/). We used Isabelle/jEdit with some latest development snapshot and bundled this as a VirtualBox VM configuration. Setting-up the system (installing VirtualBox, importing the VM configuation) in most cases took less than 10 minutes, which we assisted in the evening the day before the tutorial session. We presented two basic examples, addition on natural number and reversal of lists, and let them work themselves with some guidance to prove one or two lemmas on their own. In the end, Johannes presented a student exercise from a first-semester undergraduate analysis course and how he would solve that with Isabelle to give the PhD students an idea what the system can do and how real proofs are developed and look like and not to leave the impression everything is proved by induct auto/simp. Overall, we got a positive feedback from many participants. Working with the interaction model of Isabelle/jEdit seemed not to pose any problem for the students and we had no crash or unexpected behaviour with the current version. I only noticed that using try you often get a misleading response from linarith that linarith found a counterexample which beginners might stumble on. It might be better to switch off this warning by default (and offer a configuration to switch it on if it is of interest). Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor
On 05/30/2011 06:03 PM, Lukas Bulwahn wrote:
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
definition test2 where test2 xs = (xs ~= [] test (rev xs))
(* Optimized implementation for test with context condition *)
lemma test_rev: xs ~= [] == test (rev xs) = (hd xs = 0)
unfolding test_def by(simp add: last_rev)
declare conj_cong[cong] test_rev[simp]
thm test2_def test2_def[simplified]
lemma test2 xs = (xs ~= [] test (rev xs))
apply simp
oops
The [simplified] attribute does apply the test_rev equation, but the
simp method in the proof does. Apparently, the same issue prevents
the code preprocessor from optimizing the code for test:
The simplifier behaves differently when working with free variables or
schematic variables.
Tobias can probably give a more precise answer how it behaves
differently (and why).
I will change the code preprocessor, so that you get the intended
behaviour.
Changeset 027ed67f5d98 enables rewriting with the declared congruence rules.
In the example above, the negation still causes problems (in your
setup), but it works if you define some predicate for xs ~= [] hiding
the negation.
Getting the setup for the code preprocessing simplifier right is of
course an exercise for its users.
It might be worth discussing if the simplified attribute should be
changed to do the same thing.
After an offline discussion with Tobias, I experimented to do the same
with the simplified attribute resulting in the following changeset:
--- a/src/Pure/simplifier.MLTue May 31 18:29:00 2011 +0200
+++ b/src/Pure/simplifier.MLTue May 31 18:32:58 2011 +0200
@@ -321,8 +321,8 @@
val simplified = conv_mode -- Attrib.thms
(fn (f, ths) = Thm.rule_attribute (fn context =
-f ((if null ths then I else Raw_Simplifier.clear_ss)
-(simpset_of (Context.proof_of context)) addsimps ths)));
+singleton (Variable.trade (fn ctxt = map (f ((if null ths then I
else Raw_Simplifier.clear_ss)
+(simpset_of ctxt) addsimps ths))) (Context.proof_of context;
end;
Unfortunately, the provided function Variable.trade renames schematic
variables (even if not necessary), making its behaviour too unexpected
for the users and causing problems with many applications in the
distribution (cf.
http://isabelle.in.tum.de/testboard/Isabelle/rev/330c709f0df9).
A Variable.trade function that at least tries to keep the same schematic
variables (in the obvious cases) would be nice for this setting. But as
long as such a function is not provided, modifying the simplified
attribute leads to problems that are not worth the benefits.
Lukas
Lukas
lemmas [code_inline] = test_rev test_rev[folded List.null_def]
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm
conj_cong}]) *}
code_thms test2
test2 is still implemented in terms of test (rev xs)
How can I unfold test_rev in test2_def?
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Congruence rules for the code preprocessor
Hi Andreas,
the following ML line should do the job of adding the congruence rule in
your case:
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm conj_cong}]) *}
Before we add yet another feature to the code generation setup in Isar,
we would like to understand your scenario.
Does it occur naturally when setting up the code generator or is it a
very special corner case in your specifications?
Lukas
On 05/29/2011 04:44 PM, Tobias Nipkow wrote:
Does the current attribute mechanism support selective attributes such
as [code_inline cong], maybe along the lines of [simp del]? If it
does, I assume it would be easy to add that information in the place
that Florian pointed to?
Tobias
Am 28/05/2011 14:45, schrieb Florian Haftmann:
Hi Andreas,
the code generator tutorial mentions that the simpset for the code
preprocessor can apply the full generality of the Isabelle simplifier.
But how can I add anything else other than unfold theorems? The
attributes code_unfold and code_inline do not accept declarations like
declare conj_cong[code_inline cong]
Is there a way in Isar to declare congruence rules to the preprocessor?
no, this can only be done on the ML level, cf.
http://isabelle.in.tum.de/reports/Isabelle/file/0f9534b7ea75/src/Tools/Code/code_preproc.ML#l10.
Maybe it would be worth thinking about transfering all simpset
declaration attributes also to code_inline.
Hope this helps,
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] [isabelle] Congruence rules for the code preprocessor
On 05/30/2011 12:33 PM, Andreas Lochbihler wrote:
Hi Lukas,
here is an example that I would have expected to work. However,
congruences seem to work other than I expected. Du you know what I am
missing here?
theory Scratch imports Main begin
definition test where test xs = (last xs = 0)
definition test2 where test2 xs = (xs ~= [] test (rev xs))
(* Optimized implementation for test with context condition *)
lemma test_rev: xs ~= [] == test (rev xs) = (hd xs = 0)
unfolding test_def by(simp add: last_rev)
declare conj_cong[cong] test_rev[simp]
thm test2_def test2_def[simplified]
lemma test2 xs = (xs ~= [] test (rev xs))
apply simp
oops
The [simplified] attribute does apply the test_rev equation, but the
simp method in the proof does. Apparently, the same issue prevents the
code preprocessor from optimizing the code for test:
The simplifier behaves differently when working with free variables or
schematic variables.
Tobias can probably give a more precise answer how it behaves
differently (and why).
I will change the code preprocessor, so that you get the intended behaviour.
It might be worth discussing if the simplified attribute should be
changed to do the same thing.
Lukas
lemmas [code_inline] = test_rev test_rev[folded List.null_def]
setup {* Code_Preproc.map_pre (fn ss = ss addcongs [@{thm
conj_cong}]) *}
code_thms test2
test2 is still implemented in terms of test (rev xs)
How can I unfold test_rev in test2_def?
Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: status (AFP)
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in the
Datatype package in the HOL image.
The complete Isabelle repository ran through (with all its datatypes),
but the Sigma theory seems to contain some unexpected datatype.
I will look at the problem immediately, and probably fix it within the
next couple of hours.
Lukas
On 04/08/2011 12:24 AM, Gerwin Klein wrote:
Can someone have a look at what is going wrong in Locally-Nameless-Sigma?
It looks like a bug in the datatype package is being triggered:
*** Stale theory encountered:
*** {Pure, Code_Generator, HOL, Orderings, Groups, Lattices, Set,
*** Complete_Lattice, Typedef, Inductive, Fun, Product_Type, Rings, Fields,
*** Sum_Type, Nat, Datatype, Complete_Partial_Order, Option, Power,
*** Finite_Set, Relation, Predicate, Transitive_Closure, Partial_Function,
*** Wellfounded, Meson, FunDef, Extraction, Metis, Plain, Big_Operators,
*** Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides,
*** Numeral_Simprocs, Semiring_Normalization, Groebner_Basis, SetInterval,
*** Hilbert_Choice, Presburger, Recdef, Code_Numeral, Quotient, ATP, List,
*** String, Typerep, Map, Random, Code_Evaluation, Enum, Lazy_Sequence,
*** Quickcheck, DSequence, Random_Sequence, New_DSequence,
*** New_Random_Sequence, Record, SMT, Sledgehammer, Refute, SAT,
*** Predicate_Compile, Quickcheck_Exhaustive, Nitpick, Main, ListPre, FMap,
*** Sigma:162, #, !}
*** At command datatype (line 80 of
/home/kleing/afp/devel/thys/Locally-Nameless-Sigma/Sigma/Sigma.thy)
Cheers,
Gerwin
Begin forwarded message:
From: Gerwin Kleinkle...@ertos.nicta.com.au
Date: 8 April 2011 6:21:49 AM AEST
To:kle...@cse.unsw.edu.au
Subject: status (AFP)
The status of the following AFP entries changed or remains FAIL:
[Locally-Nameless-Sigma] is still on FAIL.
Full entry status at http://afp.sourceforge.net/status.shtml
AFP version: development -- hg id 29a8783494d0
Isabelle version: devel -- hg id 7d08265f181d
Test ended on: lemma, Fri Apr 8 06:21:49 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
___
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 04/08/2011 01:03 PM, Stefan Berghofer wrote: Quoting Lukas Bulwahn bulw...@in.tum.de: Hi, My changes caused this error. I am working on different compilation schemes in Quickcheck. Quickcheck registers its type-class based generator construction in the Datatype package in the HOL image. Hi Lucas, according to the trace, the exception occurs somewhere in the function derive_datatype_props in datatype_data.ML. When taking a quick look at the code, I noticed that thy2 is used in two places (lines 311 and 322) after it has already been modified. Is that intentional, or could this be related to this bug, too? Hi Stefan, Thanks for your effort. I have already fixed the error (on my local machine) -- it was actually related to some exception handling that has never been working, but was never triggered before this changeset. Lukas Greetings, Stefan ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Fwd: [isabelle] list_to_set_comprehension bug ?
On 01/19/2011 03:41 PM, Mathieu Giorgino wrote:
Hello all,
It seems there is a problem with the list_to_set_comprehension tactic for
terms containing a pattern matching on a datatype with a single constructor
with at least three arguments (It appears as a rather specific problem...).
datatype t = T unit unit unit
(* declare [[ simproc del: list_to_set_comprehension ]] *)
lemma set (case n of T a b c ⇒ [b]) ≠ {}
by (auto split:t.splits) (* *** Tactic failed *)
Is this a bug ?
It is indeed a bug - Thanks for reporting.
I have already fixed it and the patch is on its way into the upcoming
release.
Lukas
Regards,
Mathieu
___
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] list_to_set_comprehension
On 01/11/2011 05:42 PM, Makarius wrote: Changes for list_to_set_comprehension keep coming in, and it seems to be not quite stabilized yet. Where is the NEWS entry that tells users what to do in case of failure? Here is the NEWS: * New simproc that rewrites list comprehensions applied to List.set to set comprehensions. To deactivate the simproc for historic proof scripts, use: [[simproc del: list_to_set_comprehension]] Yesterday I have tried to sanitize AFP/JinjaThreads in other repsects, but it did not work (the approximative versions are Isabelle/2aec4b8cd289 AFP/6ac7d314792d). I have worked on Jinja and committed this morning (60003ac7ecd5: fixing Jinja theory due to new list_to_set_comprehension simproc). I fail to build the JinjaThreads image on my local machine, but I do follow the AFP status reports. 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] Declaration depending on user proofs
On 10/07/2010 09:11 AM, Florian Haftmann wrote:
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 = 'b_1) = ... = ('a_n = 'b_n)
= ('a_1, ..., 'a_n) k is = ('b_1, ..., 'b_n) k
for an n-ary type ('a_1, ..., 'a_n) k must satisfy some characteristic
properties like
map_k f_1 ... f_n o map_k g_1 ... g_n =
map_k (f_1 o g_1) ... (f_n o g_n)
To declare something as a type mapper, the following command could be
introduced
type_mapper map_k
proof
which would issue an appropriate declaration. Attributes are
inappropriate here since the user cannot be expected to write down the
theorems to prove explicitly.
However I am always reluctant to introduce new keywords, both for
aesthetic and technical reasons. So I am asking myself whether we
should introduce a command for generic user-proof-dependent
declarations, e.g.
proveargs
proof
Here different parsers could be registered under the umbrella of the
same command. Some possible instances:
prove type_mapper: map_l
proof
prove isomorphism: Fset.Fset Fset.member
proof
Any opinions?
Florian
The code_pred command for the invocation of the predicate compiler could
also fit under this umbrella.
So the syntax would change from code_pred to prove code_pred which
is actually better, because then users are not surprised
that the command sets up some goal state (in most cases the empty goal)
for the user to prove.
Lukas
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
