Re: [isabelle-dev] Gromov Hyperbolicity
On Thu, 2018-01-18 at 14:31 +0100, Tobias Nipkow wrote: > > One possible criterion: which results > > are part of a standard undergraduate athematics curriculum? > > It sounds like a reasonable criterion. Can you tell us what that means for > Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)? Metric completion features prominently, e.g., in the construction of the reals. Lipschitz continuity (along with the Picard–Lindelöf theorem) should be part of any course on differential equations. I can't recall whether I've been taught about Hausdorff distance or even isometries during my undergraduate years. Of course, these are fairly simple concepts. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] not-exists problem
On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote: > I would have expected: > (∄x y. P x y) ⟷ ¬(∃x y. P x y) > and > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x)) +1 Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Factorial ring
Florian, On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote: > "multiplicity" is definitely interesting [...] > I don't see why is_prime should require an algebraic_semidom [...] > Factorial rings (also known as unique factorisation domains) usually > [...] > [...] (somewhat non-standard) normalization_semidom. My general impression is that it would be good if the algebraic hierarchy that is part of standard Isabelle/HOL could follow standard mathematical definitions and nomenclature more closely. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: new internal proof-producing SAT solver
Makarius,
On Fri, 2014-05-09 at 12:00 +0200, Tjark Weber wrote:
Moreover, it is merely a historic accident that the theory is based on
Refute. [...]
I am attaching a patch that replaces Refute with Nitpick in
HOL/ex/Sudoku.thy.
Best,
Tjark
# HG changeset patch
# User webertj
# Date 1399846418 -7200
# Mon May 12 00:13:38 2014 +0200
# Node ID 0e2e4d38212a1a07c3ec392a0e4e7ab0815d6ff2
# Parent 6dd8866eca693a8f4df76b0a6f5a5df1a5befa86
Replaced refute with nitpick.
diff -r 6dd8866eca69 -r 0e2e4d38212a src/HOL/ROOT
--- a/src/HOL/ROOT Sun May 11 20:23:08 2014 +0200
+++ b/src/HOL/ROOT Mon May 12 00:13:38 2014 +0200
@@ -581,13 +581,11 @@
Simps_Case_Conv_Examples
ML
SAT_Examples
+Sudoku
theories [skip_proofs = false]
Meson_Test
theories [condition = SVC_HOME]
svc_test
- theories [condition = ZCHAFF_HOME]
-(*requires zChaff (or some other reasonably fast SAT solver)*)
-Sudoku
document_files root.bib root.tex
session HOL-Isar_Examples in Isar_Examples = HOL +
diff -r 6dd8866eca69 -r 0e2e4d38212a src/HOL/ex/Sudoku.thy
--- a/src/HOL/ex/Sudoku.thy Sun May 11 20:23:08 2014 +0200
+++ b/src/HOL/ex/Sudoku.thy Mon May 12 00:13:38 2014 +0200
@@ -1,24 +1,23 @@
(* Title: HOL/ex/Sudoku.thy
Author: Tjark Weber
-Copyright 2005-2008
+Copyright 2005-2014
*)
header {* A SAT-based Sudoku Solver *}
theory Sudoku
-imports Main ../Library/Refute
+imports Main
begin
text {*
- Please make sure you are using an efficient SAT solver (e.g., zChaff)
- when loading this theory. See Isabelle's settings file for details.
+ See the paper ``A SAT-based Sudoku Solver'' (Tjark Weber, published at
+ LPAR'05) for further explanations. (The paper describes an older version of
+ this theory that used the model finder @{text refute} to find Sudoku
+ solutions. The @{text refute} tool has since been superseded by
+ @{text nitpick}, which is used below.)
+*}
- Using zChaff, each Sudoku in this theory is solved in less than a
- second.
-
- See the paper A SAT-based Sudoku Solver (Tjark Weber, published at
- LPAR'05) for further explanations.
-*}
+no_notation Groups.one_class.one (1)
datatype digit = A (1) | B (2) | C (3) | D (4) | E (5) | F (6) | G
(7) | H (8) | I (9)
@@ -98,11 +97,11 @@
x71 x72 x73 x74 x75 x76 x77 x78 x79
x81 x82 x83 x84 x85 x86 x87 x88 x89
x91 x92 x93 x94 x95 x96 x97 x98 x99
- refute
+ nitpick [expect=genuine]
oops
text {*
- An easy Sudoku:
+ An ``easy'' Sudoku:
*}
theorem \not sudoku
@@ -115,11 +114,11 @@
x71 6 x73 x74 x75 x76 2 8 x79
x81 x82 x83 4 1 9 x87 x88 5
x91 x92 x93 x94 8 x96 x97 7 9
- refute
+ nitpick [expect=genuine]
oops
text {*
- A hard Sudoku:
+ A ``hard'' Sudoku:
*}
theorem \not sudoku
@@ -132,13 +131,13 @@
x71 x72 x73 x74 1 x76 7 8 x79
5 x82 x83 x84 x85 9 x87 x88 x89
x91 x92 x93 x94 x95 x96 x97 4 x99
- refute
+ nitpick [expect=genuine]
oops
text {*
- Some exceptionally difficult Sudokus, taken from
+ Some ``exceptionally difficult'' Sudokus, taken from
@{url
http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudokuoldid=254685903}
- (accessed December 2, 2008).
+ (accessed December~2, 2008).
*}
text {*
@@ -172,7 +171,7 @@
7 x72 x73 x74 x75 x76 6 x78 x79
x81 3 x83 x84 x85 9 x87 8 x89
x91 x92 2 x94 x95 x96 x97 x98 1
- refute
+ nitpick [expect=genuine]
oops
text {*
@@ -206,7 +205,7 @@
3 x72 x73 x74 8 x76 x77 x78 6
x81 x82 9 2 x85 x86 x87 x88 x89
x91 4 x93 x94 x95 1 x97 x98 x99
- refute
+ nitpick [expect=genuine]
oops
text {*
@@ -240,7 +239,7 @@
x71 x72 9 x74 8 x76 x77 5 x79
x81 2 x83 x84 x85 x86 6 x88 x89
4 x92 x93 7 x95 x96 x97 x98 x99
- refute
+ nitpick [expect=genuine]
oops
text {*
@@ -274,7 +273,7 @@
5 x72 x73 x74 x75 x76 9 x78 x79
x81 3 x83 9 x85 x86 x87 x88 7
x91 x92 1 x94 x95 8 6 x98 x99
- refute
+ nitpick [expect=genuine]
oops
text {*
@@ -308,7 +307,7 @@
x71 x72 9 x74 8 x76 x77 5 x79
x81 2 x83 x84 x85 x86 6 x88 x89
4 x92 x93 7 x95 x96 x97 x98 x99
- refute
+ nitpick [expect=genuine]
oops
end
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: new internal proof-producing SAT solver
On Wed, 2014-05-07 at 15:41 +0200, Makarius wrote: How about ~~/src/HOL/ex/Sudoko.thy? It formally depends on ZCHAFF_HOME, so it is rarely run in practice. Does it now make sense to remove that condition in the ROOT file? What is tested in this theory anyway? The 'refute' / 'oops' sequences seem to be relatively soft in their requirements. The theory demonstrates how Isabelle can be used as an efficient Sudoku solver. zChaff is still clearly superior to the internal solver ( 1s vs. 60s for some problems in this theory). But the worst that should happen with the internal solver are timeouts within Refute. I suppose if you don't mind burning a few cycles, the condition in ROOT could be dropped. Moreover, it is merely a historic accident that the theory is based on Refute. I tried switching to Nitpick just now, but I ran into a minor issue that I'll raise in a separate thread. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Safe approach to hypothesis substitution mark II
On Mon, 2014-01-13 at 12:38 +, Thomas Sewell wrote: Given a hypothesis of the form x = Suc a or Suc a = x, where x is a free (blue) variable, hypsubst will substitute Suc a for x throughout the goal, and then discard the hypothesis. The substitution is almost always wanted. Discarding the hypothesis may, however, be unsafe, since there may be facts about x at the proof or locale level that now cannot be used. It may also be unsafe in the subtle case where a schematic variable in the goal can be instantiated to functions of x but not of Suc a. This unsafeness is undesirable because hypsubst is called from tactics that are meant to be safe. I will freely admit my ignorance of the issues involved, but perhaps it would be desirable to identify these unsafe situations in the code and discard the hypothesis if (and only if) doing so is safe? Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle dimacs2hol
On Thu, 2013-08-01 at 16:41 +0200, Makarius wrote: On Wed, 10 Jul 2013, Tjark Weber wrote: Looking superficially at http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy I wonder if this actually works right now. Good question. One issue is that the theory requires a SAT solver (zChaff or MiniSat) to work properly. These days, one could probably be shipped as a component, but I wonder if that's worth it. People just don't seem to use Isabelle to prove large propositional tautologies. I still think that encodings of decidable problems into propositional logic could probably be just as beneficial in theorem proving as they've been in many other domains. But regarding the future of sat, I am rather undecided at this point. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Subscripts within identifiers
On Fri, 2013-07-12 at 19:41 +0200, Makarius wrote: How would Omega Algebras fare with notation A\^sup\infinity instead of A\^sup\omega? Worse. Of course, a name is just that, but for clarity and convenience, it is nice to be able to call things in Isabelle what they are called in the literature. For serious output (e.g., papers), A\^sup\infinity instead of A\^sup\omega would demand further post-processing. Best, Tjark signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
Larry, On Thu, 2013-05-02 at 16:18 +0100, Lawrence Paulson wrote: I am getting a lot of poly/ML segmentation faults, and they are making it very difficult to do my work, especially as my theories take at least 15 minutes to load. If it then simply crashes then I'm not getting anywhere. Has anybody else had this problem with Poly/ML? Since nobody else replied: I do get occasional segfaults from Poly/ML (not only running Isabelle, but also other ML code). David Matthews is usually quite responsive to bug reports. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
Johannes, On Mon, 2013-04-22 at 16:39 +0200, Johannes Hölzl wrote: * Introduce type class conditional_complete_lattice: Like a complete lattice but does not assume the existence of the top and bottom elements. The name conditional complete lattice suggests a special kind of complete lattice. However, without top and bottom elements, this structure is not a complete lattice at all. In the literature, it is therefore more aptly called conditionally complete lattice. I propose to retain the -ly suffix in the name of the type class. Best, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Very counterintuitive set notation for tuples, introducing new variable without warning
On Fri, 2013-03-22 at 13:25 +0100, Makarius wrote:
On Fri, 22 Mar 2013, Andreas Lochbihler wrote:
{(x, y). P} is pretty syntax for
Collect (prod_case (%x y. P)), so in your case, you get
Collect (prod_case (%v v. v : {''a'', ''b''}))
See how the second v in %v v. ... hides the former.
There is no warning because it is perfectly normal to rebind a variable
name in a lambda abstraction.
I agree that it is perfectly normal, just like term λx x x. x, and no
warning or error is to be expected.
Clearly, different people have different expectations. {(v,v). P v}
is not a lambda abstraction (regardless of how it is represented
internally). But it is similar to established mathematical notation, so
users might (and, as this thread again shows, do) expect it to denote
some subset of the identity relation. See also
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-April/msg00028.html
Best,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Automated testing questions
On Mon, 2013-03-18 at 12:16 +0100, Makarius wrote: If anything is missing or wrong in README_REPOSITORY, I ask once again to point it out, either on isabelle-dev or privately, and not to make unreliable/unmaintained clones of such important information. Occasionally cd isabelle hg pull -u ./bin/isabelle components -a ./bin/isabelle jedit -l HOL results in Scala build errors. If this is bound to happen from time to time, instructions on how to recover (possibly just mentioning -f) or a pointer to such instructions might be helpful. Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Build error: isabelle.XML$XML_Body
Hi, After hg fetch to update to tip (22ba938ab10f), followed by isabelle components -a, Isabelle build now fails with this error message: isabelle.XML$XML_Body Any advice? Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Build error: isabelle.XML$XML_Body
On Fri, 2013-02-22 at 13:26 +0100, Makarius wrote: I would say you just need the usual isabelle build -b -f to force a fresh build of everything. Java stuff, and especially Scala stuff is not 100% monotone wrt. upgrades. Thanks for the quick reply. jedit -b -f by itself didn't seem to fix the issue, but after manually deleting files in ~/.isabelle/ I am no longer stuck. (I did run into the problem that Christian Sternagel noticed recently, where afp_build failed to update session index, but managed to solve that myself.) Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] the sound of a sledgehammer
On Fri, 2013-02-15 at 13:37 +0100, Tobias Nipkow wrote: * Sledgehammer spontaneously acts asynchronously of certain open problems in the text, depending on certain parameters like time outs. Triggering s/h via sorry (or some other explicit means) is perfectly reasonable, but having the IDE invoke s/h based on time outs and guesses should be avoided: the success rate is low and it consumes a lot of resources. My gut feeling is that already today, I would prefer s/h to run automatically on every intermediate proof state if this didn't interfere with my editing. Why should the many cores in my machine sit idle? It seems perfectly reasonable to spend a few billion CPU cycles if that occasionally saves a minute or two of human time. Architecturally, some kind of incremental mode for s/h (as suggested by Jasmin) could reduce the performance overhead. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Hi Jasmin, On Wed, 2013-02-13 at 09:09 +0100, Jasmin Christian Blanchette wrote: Thankfully, there's a much easier solution: using [[metis_verbose = false]] by (metis ...) or, at the top-level, declare [[metis_verbose = false]] It's always nice to find out that a requested feature already exists. Thanks again! Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Hi Jasmin, On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote: To suppress the warning, one trick is to ensure that the theorem has no name hint, e.g. mythm[THEN asm_rl] or (if it's not polymorphic) pipe it in with using mythm apply -. The first trick could be made cleaner through a new attribute, e.g. silent or nameless. This continues to be a very minor issue, but perhaps it's still useful if I share my findings. The good news first: there already is an attribute to drop the name hint, namely ...[untagged name] Now the bad news: just like your suggestion of [THEN asm_rl], this doesn't get rid of the metis warning, but merely changes it to Unused theorems: ??.unknown Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
On Wed, 2013-01-30 at 15:14 +0100, Jasmin Christian Blanchette wrote: First is quite a bit of work, if you want to bring it into a format that Joe Hurd can understand, assuming he even has the time to look into it. It's probably not worth the effort then. Like you said, this kind of behavior can happen. To suppress the warning, one trick is to ensure that the theorem has no name hint, e.g. mythm[THEN asm_rl] Good to know that there is a workaround. [*] A rule of thumb I remember from industry was to wait until we had the same feature request at least three times before implementing anything. That of course made more sense w.r.t. a large user base (~ 10 000 to 100 000) than for the Isabelle community. Some projects let users vote (+1) on feature requests. Of course, as Steve Jobs put it: A lot of times, people don't know what they want until you show it to them. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
On Fri, 2013-01-18 at 19:29 +0100, Jasmin Christian Blanchette wrote: What's your concrete suggestion here? It's more of a curiosity than an issue, of course. Otherwise, I would suggest to: First, make sure that the behavior is not due to a bug or silly inefficiency in the metis code. Second, offer a way to suppress the warning. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Hi, The new AFP entry on Kleene Algebras contains a metis call (http://afp.hg.sourceforge.net/hgweb/afp/afp/file/082b389cb3f8/thys/Kleene_Algebra/Kleene_Algebra.thy#l652) that generates a warning about an unused theorem local.opp_mult_def. Not passing opp_mult_def as an argument to metis gets rid of the warning, but increases run-time of this metis call from ~ 1 s to ~ 15 s on my machine. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Testing AFP at TUM
On Sun, 2012-10-21 at 16:46 +0200, Florian Haftmann wrote: Btw. whenever I'm testing the AFP these days without relying on the testboard I use the following [...] In the last few months I've seen several emails with testing advice on this list (occasionally motivated by commits that apparently hadn't been tested very thoroughly). Perhaps it would be useful to distill these into a concise description of current best practice; either as part of README_REPOSITORY or in the Isabelle Wiki? Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] HOL/Rings.thy: {left,right}_distrib
On Tue, 2012-10-16 at 17:43 +0200, Tobias Nipkow wrote: Am 16/10/2012 13:22, schrieb Tjark Weber: Class semiring in HOL/Rings.thy [1] assumes left_distrib: (a + b) * c = a * c + b * c right_distrib: a * (b + c) = a * b + a * c We should certainly not contradict the mathematical usage. I favour Jasmin's proposal because distributivity is such a well-known notion that I would not like to get rid of it. [...] See now Isabelle/a8cc904a6820 and AFP/b162ed761092. Please let me know if anything breaks; these theorem names were used all over the place. There are other occurrences of left/right distributivity theorems (e.g., for setsum), both in theories and in ML sources. I haven't touched those, so at least some of them probably still follow the above unconventional naming scheme. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Locale interpretation with mixins
On Fri, 2012-09-07 at 17:20 +0200, Makarius wrote: So when the code generator sees an interpreted function application loc.c t1 t2 t3 x y z it should somehow do the right thing, in taking it as (loc.c t1 t2 t3) x y z, and considering the inner part as atomic entity (and instance of c defined earlier in the abstract context). I recently asked (somewhat clumsily, and not in the context of code generation) about essentially the same issue: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-August/msg00218.html So this is not restricted to code generation or simplification, but (unsurprisingly) also shows up in other applications. When there is a recommended way of doing the right thing here, I'd be grateful for a pointer. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
On Mon, 2012-08-27 at 13:35 +0200, Makarius wrote: 1) In theory T imports A, I'd like to be able to Ctrl-click on A to open the corresponding theory file. See some changesets leading up to Isabelle/10b89c127153 how I've spent Sunday afternoon. Nice. I suspect it would be considerably more work to support C-click in already loaded theories (e.g., HOL/Main)? Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] download-components
Christian, On Wed, 2012-08-08 at 14:17 +0900, Christian Sternagel wrote: the script you introduced in http://isabelle.in.tum.de/repos/isabelle/rev/c895e334162c is rather useful. How about also providing a variable (as TMP for the download directory) to set the actual isabelle tool (with default isabelle) instead of hard-wiring isabelle (which does not work all too well, when having different isabelle versions installed)? see now http://isabelle.in.tum.de/repos/isabelle/rev/cea7f88c8084 as a first step. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] download-components
On Wed, 2012-08-08 at 11:22 +0200, Makarius wrote: One could also use wget -O- ... | tar xvzf - and avoid the TMP file. Unfortunately, this doesn't behave as one would like when wget fails. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] download-components
On Wed, 2012-08-15 at 13:22 +0200, Makarius wrote: I will have to take a look at the component business again soon, to simplify it further and remove features and clones of other Isabelle scripts. Great. I've now turned download_components into an isabelle (Admin) tool (cf. 01d1734f779d), as you suggested. Feel free to make further refinements. Best regards, Tjark -- Ceterum censeo: Isabelle needs an issue tracker. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Incomplete .hgignore?
Hi, Building the repository version (7476665f3e0f) with isabelle build -a generates a number of files that Mercurial doesn't know about (see below). I could simply add them to .hgignore, but perhaps someone who knows why these files are generated would be more qualified to do so? Best regards, Tjark $ bin/isabelle build -a [...] $ hg status ? doc-src/Classes/Thy/document/Code_Integer.tex ? doc-src/Classes/Thy/document/Code_Natural.tex ? doc-src/Classes/Thy/document/Setup.tex ? doc-src/Classes/Thy/document/session.tex ? doc-src/Codegen/Thy/document/Setup.tex ? doc-src/Codegen/Thy/document/session.tex ? doc-src/Codegen/Thy/examples/rat.ML ? doc-src/Functions/Thy/document/session.tex ? doc-src/IsarImplementation/Thy/document/session.tex ? doc-src/IsarRef/Thy/document/Base.tex ? doc-src/IsarRef/Thy/document/Old_Recdef.tex ? doc-src/IsarRef/Thy/document/Wfrec.tex ? doc-src/IsarRef/Thy/document/session.tex ? doc-src/LaTeXsugar/Sugar/document/session.tex ? doc-src/Main/Docs/document/session.tex ? doc-src/ProgProve/Thys/document/MyList.tex ? doc-src/ProgProve/Thys/document/session.tex ? doc-src/System/Thy/document/session.tex ? doc-src/TutorialI/document/Basic.tex ? doc-src/TutorialI/document/Binomial.tex ? doc-src/TutorialI/document/Blast.tex ? doc-src/TutorialI/document/Examples.tex ? doc-src/TutorialI/document/Force.tex ? doc-src/TutorialI/document/Forward.tex ? doc-src/TutorialI/document/Functions.tex ? doc-src/TutorialI/document/Primes.tex ? doc-src/TutorialI/document/Recur.tex ? doc-src/TutorialI/document/Relations.tex ? doc-src/TutorialI/document/Setup.tex ? doc-src/TutorialI/document/Tacticals.tex ? doc-src/TutorialI/document/session.tex ? doc-src/ZF/document/FOL_examples.tex ? doc-src/ZF/document/IFOL_examples.tex ? doc-src/ZF/document/If.tex ? doc-src/ZF/document/ZF_examples.tex ? doc-src/ZF/document/session.tex ? src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.prv ? src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_l.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_r.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_l.prv ? src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_r.prv ? src/HOL/SPARK/Examples/Sqrt/sqrt/isqrt.prv ? src/HOL/SPARK/Manual/complex_types_app/initialize.prv ? src/HOL/SPARK/Manual/loop_invariant/proc1.prv ? src/HOL/SPARK/Manual/loop_invariant/proc2.prv ? src/HOL/SPARK/Manual/simple_greatest_common_divisor/g_c_d.prv -- Ceterum censeo: Isabelle needs an issue tracker. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Incomplete .hgignore?
On Tue, 2012-08-14 at 17:09 +0200, Makarius wrote: Building the repository version (7476665f3e0f) with isabelle build -a generates a number of files that Mercurial doesn't know about (see below). That is normal for people who are used to build the doc-src stuff occasionally. The difference is that it is now part of the regular build. .hgignore should not be abused to hide that mess, otherwise the issue gets swepped under the carpet. (AFP had some issues recently because of too liberal .hgignore.) If these files are intentionally generated in isabelle/.../ and not meant to be under version control, I am not sure I see the abuse in adding them to .hgignore. On the other hand, if they are a mess and an issue, perhaps that could be addressed. Anyway, what do you do to keep the output of hg status uncluttered? Best regards, Tjark -- Ceterum censeo: Isabelle needs an issue tracker. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle/jEdit: Feature Requests for Ctrl-Click
Hi,
Ctrl-click in Isabelle/jEdit exposes additional information - about
the next best thing since sliced bread. I have a few suggestions for
related features that would be nice to have, in my opinion (provided
they are not too much implementation work):
1) In theory T imports A, I'd like to be able to Ctrl-click on A to
open the corresponding theory file.
2) In use filename, I'd like to be able to Ctrl-click on filename to
open the corresponding file.
3) In ML {* open Foo; *}, I'd like to be able to Ctrl-click on Foo to
see its definition.
4) Ctrl-click on an ML identifier takes me to its declaration (typically
in some signature). Wouldn't it be more useful to be taken to its
definition (i.e., the actual implementation, typically in a structure)?
Best regards,
Tjark
--
Ceterum censeo: Isabelle needs an issue tracker.
___
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 Tue, 2012-06-26 at 22:46 +0200, Florian Haftmann wrote: Tiny instructions on changesets c97656ff4154 ff.: [...] The Isabelle Wiki has a HOWTO on Working with the repository version of Isabelle (at https://isabelle.in.tum.de/community/Working_with_the_repository_version_of_Isabelle). Perhaps you could update the section on Initializing auxiliary components? Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle release test website
On Thu, 2012-04-26 at 14:09 +0200, Makarius wrote: The website itself is starting to take shape. Thanks to Johannes Hölzl we now have nice download buttons that detect the platform of the web browser: Linux, Linux 64 bit, Mac OS X, Windows. All 4 buttons are shown if the platform cannot be detected. There is the (uncommon, perhaps, but not completely absurd) use case where a user wants to download a version for another platform, different from the one she is currently running. To support this, it might be better to have a drop-down list that is initialized to the detected platform, or to add an explicit download link to the other versions. That they are available (only) under Installation instructions is somewhat counter-intuitive. Best regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] canonical left-fold combinator for lists
On Sat, 2012-01-14 at 14:34 +0100, Tobias Nipkow wrote: - If one of them is singled out as fold, then it should be foldr, not foldl [...] This is correct, of course; also because foldr can be generalized to catamorphisms on arbitrary algebraic data types. In other words, foldr is the canonical fold. ;-) However, for clarity I would suggest to go with foldl/foldr rather than foldl/fold. Kind regards, Tjark ___ 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 – feasibility study
On Thu, 2011-08-18 at 09:34 +0200, Jasmin Christian Blanchette wrote: The maintenance load is extremely low. When it comes to the REFUTE exception, I can look at it if and when we decide to move back to sets. I suspect that Jasmin will have no trouble fixing this, but otherwise I'd be happy to look into it as well. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode
On Tue, 2011-07-05 at 13:27 +0200, Gerwin Klein wrote: 500: 643.64 3421.79 I may be stating the obvious, but in my (general) experience, profiling large examples like these (and subsequent code optimization) can often lead to drastic performance improvements if it hasn't been done before. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] unhelpful low-level error message from primrec
On Sat, 2011-05-21 at 15:12 -0700, Brian Huffman wrote: I just noticed this error message from primrec [...] What is the status of primrec anyway, in the light of fun(ction)? Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] fun f where f 0 = ... raises TYPE
Hi, Attempting to define fun f where f 0 = undefined in Isabelle/HOL (7f2793d51efc) yields *** exception TYPE raised (line 38 of .../isabelle/src/HOL/Tools/Function/pattern_split.ML): inst_constrs_of *** At command fun A more user-friendly error message would be nice. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Problem with frule_tac substitution
On Tue, 2011-02-08 at 06:53 -0800, Brian Huffman wrote: Honestly, I think the above parsing rules are quite confusing, and should be changed. I instantiate variables in theorems quite often, and many theorems use variable names that end in digits, but I almost never need to refer to variables with indices other than 0. For what it's worth, I agree with Brian here. I remember that this was one of the minor hurdles when I first encountered Isabelle -- the kind of technicality that can take a new user anywhere from 5 minutes to \infty to figure out. Changing the current behavior in my humble opinion would be an improvement. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Sort Annotation vs. Class Context for Lemmas
Hi, I noticed that numerous lemmas in HOL that refer to class constants are stated at the top level (using implicit or explicit sort annotations), rather than in the corresponding class context (see, for instance, Compl_lessThan in HOL/SetInterval.thy). If I am not mistaken, this means the corresponding lemma is not available in the context of the class, which seems unfortunate. Is this merely a legacy issue, or are there genuine reasons for stating these lemmas with sort annotations? Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas
On Fri, 2011-01-21 at 15:27 +0100, Tobias Nipkow wrote: One issue can be that if some sort involves multiple type classes, the corresponding class may not have been defined. That is the one advantage of sorts: you can create conjunctions/intersection of type classes on the fly. If there is just one intersection of type classes, one should perhaps consider defining the corresponding class (before stating the lemma in its context). The alternative is that the poor user who later feels that this class would be really useful has to re-prove every lemma. Of course, this doesn't work for lemmas that involve separate sorts. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Sort Annotation vs. Class Context for Lemmas
On Fri, 2011-01-21 at 07:27 -0800, Brian Huffman wrote:
On Fri, Jan 21, 2011 at 7:03 AM, Tjark Weber webe...@in.tum.de wrote:
Of course, this doesn't work for lemmas that involve separate sorts.
I'm not sure if this is what you have in mind, but in HOLCF there is a
continuity predicate
cont :: ('a::cpo = 'b::cpo) = bool
which of course is impossible to define or reason about within the
context of any single class (unless you do some weird mixing of
locale- and class-based reasoning). The same goes for the mono
predicate in the main HOL libraries. So it is clear that locale
contexts are quite restrictive compared to stating lemmas with type
class constraints.
Of course. (What I had in mind was more along the lines of 'a::A,
'b::B, but your example is even nicer.)
But anyway, let me step back a bit and ask a higher-level question:
Why do you need to prove lemmas *in* the context of a class at all?
Well, to enable what the class tutorial calls abstract reasoning, that
is, transfer of theorems to interpretations and sublocales.
Kind regards,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Accented characters
On Thu, 2011-01-13 at 22:15 +1100, Gerwin Klein wrote: On 13/01/2011, at 8:51 PM, Larry Paulson wrote: Accented characters on our website no longer display correctly on Macs. I don't know precisely when this happened, but I'm sure it's fairly recent. In fact, the characters don't even display correctly in the HTML source. It may be a character encoding problem. Clearly, it renders correctly in Google Chrome but not in Firefox or Safari. The issue also shows up on Linux. This issue is a bit strange. It shows up on my Mac as in your picture from the Cambridge server, but it looks fine with the correct characters from the Munich and Sydney servers. It may have more to do with what the server expects as encoding in the source file than what the browser gets to see. Indeed this appears to be a configuration issue with the Cambridge web server. For some of my personal pages (also delivered from Cambridge), the W3C validator shows a warning The character encoding specified in the HTTP header (utf-8) is different from the value in the meta element (iso-8859-1). So it would seem that the Cambridge web server erroneously expects all web pages to be UTF-8 encoded. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] [rt.cl.cam.ac.uk #73409] AutoReply: Re: Accented characters
This message has been automatically generated in response to the creation of a trouble ticket regarding Re: [isabelle-dev] Accented characters, a summary of which appears below. There is no need to reply to this message immediately. Your ticket has been assigned an ID of [rt.cl.cam.ac.uk #73409]. Please include this in the subject line of all future correspondence about this issue. To do so, you may reply to this message. sys-ad...@cl.cam.ac.uk - On Thu, 2011-01-13 at 22:15 +1100, Gerwin Klein wrote: On 13/01/2011, at 8:51 PM, Larry Paulson wrote: Accented characters on our website no longer display correctly on Macs. I don't know precisely when this happened, but I'm sure it's fairly recent. In fact, the characters don't even display correctly in the HTML source. It may be a character encoding problem. Clearly, it renders correctly in Google Chrome but not in Firefox or Safari. The issue also shows up on Linux. This issue is a bit strange. It shows up on my Mac as in your picture from the Cambridge server, but it looks fine with the correct characters from the Munich and Sydney servers. It may have more to do with what the server expects as encoding in the source file than what the browser gets to see. Indeed this appears to be a configuration issue with the Cambridge web server. For some of my personal pages (also delivered from Cambridge), the W3C validator shows a warning The character encoding specified in the HTTP header (utf-8) is different from the value in the meta element (iso-8859-1). So it would seem that the Cambridge web server erroneously expects all web pages to be UTF-8 encoded. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [rt.cl.cam.ac.uk #73409] Re: Accented characters
On Thu, 2011-01-13 at 11:48 +, Piete Brooks via RT wrote: Indeed this appears to be a configuration issue with the Cambridge web server. See http://www.cl.cam.ac.uk/news/2011/01/web-server-changes/ I am surprised that the web server cannot be configured to add the UTF-8 default encoding only when the page doesn't declare its own encoding. In any case, thanks for your quick and very helpful reply! Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Local Specification Mechanisms: Brief Experience Report
Clemens, Thanks for your quick reply! On Thu, 2010-12-16 at 20:37 +0100, Clemens Ballarin wrote: Suggestions? The message also says that the relation is probably not terminating. Well, roundup bound is developer jargon. Sublocale relation probably not terminating points into the right direction, but is not very precise (because cyclic sublocale relations are, in general, permitted). Most importantly, any indication on how to resolve the problem is missing. So here's an attempt: | Sorry, Isabelle cannot establish the requested sublocale relationship | because the effected chain of interpretations would be too long. | | Please try to establish a different sublocale relationship. | Section 7.1 of the Tutorial to Locales and Locale Interpretation | provides further information on how to avoid infinite chains of | interpretations. (With a more closely integrated help system, further information would be only one click away. Moreover, Isabelle could automatically suggest a sublocale statement that breaks the cycle. But I'm dreaming; other features are more important, of course.) lemma class.X (undefined x) sorry I'm afraid I don't understand why this is a workaround. It establishes the logical content of the sublocale relationship (i.e., the corresponding proof obligation), without providing any interpretations however. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Local Specification Mechanisms: Brief Experience Report
I've recently worked on an algebraic hierarchy, ranging from semi-groups to Kleene algebras and related structures, in Isabelle/HOL. It goes without saying that Isabelle's local specification mechanisms were well suited for the task. However, using classes and locales more extensively for the first time, I noticed some (possibly well-known) shortcomings. Perhaps by sharing my initial observations and the pitfalls that I ran into, I can provide some inspiration for further improvement. My intention is not to tread on someone's toes in the process; apologies if I do. Anyway, here we go (all based on Isabelle 2009-2): * The documentation for local specification mechanisms is not very homogeneous. The tutorials on type classes and locales are valuable. From a user's perspective, however, a unifying discussion (with guidance on when to use which) is missing. (This is probably a natural consequence of the fact that Isabelle's local specification mechanisms were developed by several people and over a long period of time.) * The previous point extends to the Isabelle/HOL library, which contains several approaches to defining algebraic hierarchies. Presumably, there is a certain amount of bit rot, and some theories that should use classes nowadays simply haven't been updated yet. * Duplicate parameter(s) in superclasses, as in class A = fixes x :: 'a class B = fixes x :: 'a class C = A + B are disallowed. The usual work-around (I believe) is to introduce a syntactic super-class X that fixes the duplicate parameter: class X = fixes x :: 'a class A = X class B = X class C = A + B This is artificial when compared to common mathematical practice, and it means that one must anticipate the entire class hierarchy whenever one introduces fixed parameters. * Class assumptions must mention the class type: e.g., class X = fixes x::'a assumes True is rejected because there is No type variable in part of specification element. Is there a technical reason for this requirement? * Cyclic sublocale relationships can lead to Duplicate fact declaration errors that are hard to understand: e.g., class X = fixes x :: 'a class A = X + assumes xxx: x = x class B = X + assumes xxx: x = x sublocale X A sorry is rejected, while class X = fixes x :: 'a class A = X + assumes xxx: x = x sublocale X A sorry class B = X + assumes xxx: x = x is accepted. Also, class X = fixes x :: 'a sublocale X X undefined . definition (in X) y == x is rejected (but accepted when the sublocale statement is qualified, as in sublocale X foo: X undefined). The error message could probably be improved. * Duplicate fact declaration errors already show up with acyclic sublocale relationships, as in class A = fixes x::'a assumes xxx: x = x class B = fixes x::'a assumes xxx: x = x sublocale A B sorry This means that one must again anticipate the entire hierarchy when naming facts. (Using a qualifier avoids the problem here, as does the use of locales instead of classes.) * Sublocale relationships that give rise to an infinite chain of instantiations, as in class X = fixes x::'a assumes x = x sublocale X X undefined x sorry cause a Roundup bound exceeded error. The error message could probably be improved. Moreover, the work-around lemma class.X (undefined x) sorry exposes what I would consider an implementation detail (namely the class predicate). It might be an idea to give the user explicit control over how many instantiation levels he wants from a sublocale command. Ceterum censeo: a bug/feature tracker would be nice to have. Kind regards, Tjark ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spike in isatest performance charts
On Fri, 2010-09-03 at 15:06 +0200, Makarius wrote: When composing log messages it is important do this from the perspective of someone who needs to figure out problems many months/years later, and needs to understand what was truely happening at some point. tuned Regards, Tjark ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Beta/Eta normalisation and net matching.
On Wed, 2010-08-04 at 11:50 +1000, Thomas Sewell wrote: It occurs to me that I don't even know whether theorems in Isabelle can be assumed to be beta/eta normal. Does anyone have any quick pointers on that? Is there a potential bug here? There are various pieces of code that expect terms and theorems to be in some kind of normal form (e.g. beta-eta), and other pieces of code that establish or preserve some kind of normal form. These invariants are often undocumented, and they have caused bugs more than once in the past. These bugs are not always trivial to hunt down either, because what you see is not what you get: Isabelle performs (some) normalization upon parsing/printing. Tjark ___ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Error message Failed to prepare dependency graph
On Tue, 2009-11-17 at 15:18 +0100, Makarius wrote: A repository clone is not a proper distribution, and various parts are missing. The Admin/build script helps to fill these gaps, notably Admin/build browser Clemens used to maintain a web page with installation instructions for the repository version of Isabelle (at http://www4.in.tum.de/~ballarin/isabelle/repository.html). Unfortunately, this page is now outdated. Still, the idea seems useful to me. Best, Tjark
[isabelle-dev] Arith fails with a Type error in application
On Fri, 2009-08-21 at 19:19 +0200, Dennis Walter wrote: The following proof works fine if QuickDirty is enabled, i.e. in interactive mode. But if this proof is re-run with QD turned off (e.g. in batch mode), the proof fails, because arith yields the error displayed below. lemma [| 1 = (a::int); 1 = (b::int) |] == 1 = a * b apply (subgoal_tac EX a' b'. a = 1 + a' b = 1 + b' 0 = a' 0 = b') apply (clarsimp simp add: ring_simps add_nonneg_nonneg mult_nonneg_nonneg) apply arith done *** Type error in application: Incompatible operand type With Toplevel.debug set, I get the following exception trace, which leads me to suspect that the problem is somewhere in presburger. Regards, Tjark == 8 == Exception trace for exception - ERROR Goal.prove_common(6)err(1) List.map(2) Goal.prove_common(6) Cooper.provelin(2) Cooper.linearize_conv(3)/3 Cooper.linearize_conv(3) Conv.combination_conv(3) Conv.combination_conv(3) Conv.combination_conv(3) Conv.then_conv(3) Conv.then_conv(3) Qelim.gen_qelim_conv(8)conv(2) Conv.combination_conv(3) Conv.combination_conv(3) Conv.then_conv(3) Qelim.gen_qelim_conv(8)conv(2) Conv.combination_conv(3) Conv.combination_conv(3) Conv.combination_conv(3) Conv.then_conv(3) Qelim.gen_qelim_conv(8)conv(2) Conv.combination_conv(3) Conv.then_conv(3) Conv.then_conv(3) Cooper.conv(2) Conv.combination_conv(3) Presburger.core_cooper_tac(1)(2) Tactical.CSUBGOAL(3) Tactical.CSUBGOAL(3) Tactical.CSUBGOAL(3) Seq.INTERVAL(4) Seq.map(2)(1) Seq.flat(1)(1) Seq.map(2)(1) Seq.flat(1)(1) Tactical.ORELSE(1)(1) Seq.map(2)(1) Seq.flat(1)(1) Seq.append(2)copy(1)(1) Seq.map(2)(1) Seq.map(2)(1) Seq.map(2)(1) Toplevel.proofs'(1)(1)(1) Runtime.debugging(2)(1) End of trace
[isabelle-dev] Isabelle NEWS as a blog ?
On Tue, 2009-07-14 at 11:19 +0200, Makarius wrote: [...] contributors are urged to document user relevant changes as soon as possible, in order that things are not forgotten for the release. (I reckon that half of the changes after Isabelle2009 have not shown up in NEWS yet.) [...] proper log entries are mainly meant to describe changes semantically to enable understanding of the history of sources many months or years later. There are quite a few things one has to keep in mind when committing changes to the Isabelle repository: announcing user-relevant changes in NEWS, making an entry in CONTRIBUTORS if appropriate, proper testing, proper formatting, etc. Is there a document that describes best practice? Should there be such a document, for (new) developers with write access to the repository? Maybe a chapter in the Isabelle Programming Tutorial would be a good place for this kind of information (unless passing it down by word of mouth is considered satisfactory, of course). Regards, Tjark
[isabelle-dev] Isabelle on Mercurial
On Sun, 30 Nov 2008, Makarius wrote: After several months of getting acquainted with distributed version control in general, we should be finally ready to switch the official Isabelle repository to Mercurial. I noticed that Mercurial does not perform CVS keyword expansion by default, causing most files in (my copy of) the repository to contain rather useless $Id$ keys now. One can argue that such keys are not necessary (since files in the repository can be identified by their changeset id); however, this is true only as long as one knows where a file is coming from. If you want keyword expansion, instructions can be found here: http://www.selenic.com/mercurial/wiki/index.cgi/KeywordExtension Best, Tjark
[isabelle-dev] Isabelle on Mercurial
On Tue, 2008-12-02 at 22:09 +0100, Makarius wrote: With Mercurial you have the whole history always around, and there is no need to encode (tiny) parts of it in the file. Certainly $Id$ keys are rather useless as long as the file is part of a managed repository. However, files escape into the wild. Outdated or incompatible file/software versions are a major source of errors. I would suggest to keep that in mind before removing version information from files altogether. (On a similar note, I would again suggest to introduce version identifiers for Isabelle theory files, to acknowledge the fact that their syntax is evolving from one Isabelle release to the next.) Best, Tjark
[isabelle-dev] An ARBITRARY question
On Fri, 2008-10-03 at 14:14 +0200, Florian Haftmann wrote: I also think that two would be better than three; technically undefined is the same as arbitrary Then what is the point of undefined_fun: undefined x = undefined in HOL.thy? Best, Tjark
[isabelle-dev] [isabelle] Incompatibilities between releases
On Fri, 2008-09-26 at 04:25 +0200, Alexander Krauss wrote: So the only realistic chance is that users keep up with the development and update their theories. Two (not necessarily great, as there is a tradeoff) ideas to assist with that: - Isabelle version headers in theory files (e.g., Developed for Isabelle 2009), possibly with Isabelle issuing a warning if missing/outdated. - More tool/script support for automatic updating of theories. (Similar to isatool fixheaders, etc. From an end-user's perspective, an automatic tool that could simply update current theory files to work with the next Isabelle version would probably be ideal. Of course such a tool might be too difficult to develop though.) Best, Tjark
