Hi Makarius,
> On 1 Jun 2018, at 23:32, Makarius wrote:
>
> On 01/06/18 10:35, Dmitriy Traytel wrote:
>> Hi all,
>>
>> thanks for pointing this out, Lars. And thanks for looking at the sources,
>> Jasmin.
>>
>> The problem seems to only show
Hi all,
thanks for pointing this out, Lars. And thanks for looking at the sources,
Jasmin.
The problem seems to only show up when the declaration in question is inside of
a class context. Here is a reduced version that does not involve primrec at all.
context linorder begin
context fixes b
Hi Larry,
in ~~/src/HOL/ROOT, the theory Probability is declared as "global". That means
that you must import it without any session qualification (just like Main or
Complex_Main).
Dmitriy
> On 2 Nov 2017, at 17:47, Lawrence Paulson wrote:
>
> I’ve been converting some
Hi Lars,
thanks for the reminder. Cf. c6714a9562ae and a5a24e1a6d6f.
Note that this still doesn’t provide the interface to Lifting and Transfer via
transfer rules for the BNF constants (which is more complicated since lift_bnf
doesn’t know about Lifting, in particular about the correspondence
Hi Makarius,
> On 24 Apr 2017, at 18:12, Makarius wrote:
>
> On 24/04/17 14:46, Makarius wrote:
>>
>> Are there users of it outside the TUM group?
My usage is the same as in Jasmin’s and Andreas’ case.
>>
>> What is good about it? What is bad about it?
>
> (1) To
Hi Makarius,
> On 10 May 2016, at 22:48, Makarius <makar...@sketis.net> wrote:
>
> On 03/03/16 14:19, Dmitriy Traytel wrote:
>
>> I wondered whether named_theorems (or more generally all dynamic facts)
>> deserve to be more visible. In particular when I search
Hi Makarius,
this is nice. At first I was a bit surprised to see the first occurrence of
list, Nil, and Cons in blue in the following datatype definitions.
datatype 'a list = Nil | Cons 'a "'a list”
But I guess, it makes sense to indicate that this is a new thing being defined.
The question
Hi Lars,
thanks for your work. Unfortunately, currently pushing to testboard/isabelle
does not seem to trigger new builds. Is this related to the job renamings?
Another renaming issue is visible here:
https://ci.isabelle.systems/status/
The status icon still points to (the now non-existent)
> On 05 Mar 2016, at 23:11, Makarius wrote:
>
> *** ML ***
>
> * Local_Theory.restore has been renamed to Local_Theory.reset to
> emphasize its disruptive impact on the cumulative context, notably the
> scope of 'private' or 'qualified' names. Note that Local_Theory.reset
Hi all,
trying the smaller audience of isabelle-dev first.
I wondered whether named_theorems (or more generally all dynamic facts) deserve
to be more visible. In particular when I search for
"(?a < ?c - ?b) = (?a + ?b < ?c)”
with find_theorems, I’d like to be reminded of algebra_simps
Maybe a guess in the blue, but here is what grep tells me:
~$ grep base_name ~/isabelle/src/HOL/Tools/ -r | grep Quick
/Users/traytel/isabelle/src/HOL/Tools//Quickcheck/abstract_generators.ML:
val name = Long_Name.base_name tyco
I have not investigated further.
Dmitriy
> On 27 Feb 2016, at
Hi Lars,
even without the slow sessions, this is of great help. Thanks!
My commit yesterday (isabelle/ae44f16dcea5) broke some AFP entries (because
without the afp_testboard, I used to follow the "break it, fix it” philosophy
w.r.t. AFP). I will repair those today.
Dmitriy
> On 17 Feb 2016,
> On 16 Feb 2016, at 11:30, Makarius <makar...@sketis.net> wrote:
>
> On Tue, 16 Feb 2016, Dmitriy Traytel wrote:
>
>> I am unsure if an Isabelle tool is the right level of abstraction for an
>> operation, only members of the isabelle (UNIX) group at TUM ca
Hi Lars,
I am unsure if an Isabelle tool is the right level of abstraction for an
operation, only members of the isabelle (UNIX) group at TUM can/should execute.
Also, wouldn’t a push to a fresh repository take quite long. (OK, negligible
compared to the actual build, but still.) And one still
Hi Lars,
great to hear!
What about having an additional afp_testboard repository where one could also
push -f changes. I am particularly interested in “slow” sessions there.
Thanks for your work,
Dmitriy
> On 30 Jan 2016, at 12:51, Lars Hupel wrote:
>
> Dear list,
>
> I'm
Hi Makarius,
here is one way to still (e1e6bb36b27a) edit the output buffer: to use the
compose key.
On my Mac, if I place the cursor into the output buffer and press alt-u
followed bei u, an ü appears in the output.
Dmitriy
> On 04 Nov 2015, at 20:42, Makarius wrote:
>
Hi Lars,
this was exactly the vision for copy_bnf, modulo that I thought of using a
plugin (“src/Pure/Tools/plugin.ML”) instead of an option. But since I am not
the author of record, I went for the less invasive option of a separate command
(in the spirit of setup_lifting for typedef). So if
Those look to me as if they have to do with 2314c2f62eb1 (real_of_nat_Suc is
now a simprule). Verified only for the Integral.thy failure.
Dmitriy
> On 06 Oct 2015, at 23:19, Makarius wrote:
>
> Here are some more proof failures (Isabelle/5b5656a63bd6 and
>
As a data point: when testing 8d40ddaa427f I could build “HOL-Proofs” in about
17 minutes.
Timing = :threads=4elapsed=979.269cpu=2582.077gc=323.518factor=2.64
Dmitriy
> On 06 Oct 2015, at 21:54, Jasmin Blanchette
> wrote:
>
> Hi Makarius,
>
>> My
The title says it all.
Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Hi,
I’m not sure if this is rather something for the jEdit mailing list, but I try
here first. The attached theory is an empty 500+ lines long file where
everything is normal. However, if I add one new line the scrollbar disappears.
The above applies to 2007ea8615a2 but I believe I saw this
) = f« prints as »curry (λ(x, y). f
x y) = f« by default.
Any headache with this?
Florian
Am 10.09.2015 um 12:19 schrieb Dmitriy Traytel:
Hi Florian,
while I very much welcome the simplified printing rules and your effort
of unifying case_prod/split, I am not sure if adding a third
Hi Florian,
while I very much welcome the simplified printing rules and your effort
of unifying case_prod/split, I am not sure if adding a third alternative
name is the way to go. The situation reminds me of the one depicted in [1].
Clearly, case_prod is the "right" name from the perspective
On 19.08.2015 22:45, Makarius wrote:
On Wed, 19 Aug 2015, Larry Paulson wrote:
I pushed a changeset to the testboard, but it isn’t showing up at
http://isabelle.in.tum.de/testboard/Isabelle
The last change it shows was 6 days ago.
Moreover, testboard and the default branch look identical
Oops, I didn't expect my name to appear here ;-)
The changeset 894d6d863823 was a reaction to Andreas Lochbihler's report
[1]. With turned off proofs the effect was a good one.
What is special about Pure.conjunction w.r.t. proof reconstruction? Is
it something in Goal.conjunction_tac? Would
I guess what Larry means is there is no way to see a type of a constant
that is not there in the source.
Consider e.g.
declare [[coercion of_nat :: nat ⇒ real]]
term sqrt (2 :: nat)
Today the output says sqrt (real_of_nat 2). But if there would be no
abbreviation for of_nat :: nat ⇒ real,
You can hover in the output panel, but you won't see types of constants
there.
Dmitriy
On 24.06.2015 16:09, Manuel Eberl wrote:
Ah, I see the problem. In that case, one could still hover over the
of_nat in the output window, but it is perhaps not ideal.
On 24/06/15 16:08, Dmitriy Traytel
Hi,
I could not believe that recdef could not be replaced by fun, so here is
the patch that removes usages of recdef from Decision_Procs. The proof
rules that come out of the function package are fine (one just needs a
few split_format (complete) attributes in a few places).
I'm not sure if
Hi Florian,
On 06.06.2015 17:11, Florian Haftmann wrote:
The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function makes
Isabelle go blue (purple)
:04, Dmitriy Traytel wrote:
Hi Andreas,
I've investigated this a bit and the slowdown happens in the code
plugin in the
instantiation of the equal type class (i.e. datatype (plugins del:
code) is more precise
than the advice below). The number of theorems proved there is
quadratic (8000 in your
tactics.
Cheers,
Andreas
On 09/04/15 15:55, Dmitriy Traytel wrote:
Hi Andreas,
rather than going dirty, try:
datatype (plugins only:) family ...
It seems that here we are lucky and the slowdown is caused by one
of the plugins. (We'll
investigate which one.)
Cheers,
Dmitriy
PS: Your datatype
Hi Andreas,
rather than going dirty, try:
datatype (plugins only:) family ...
It seems that here we are lucky and the slowdown is caused by one of
the plugins. (We'll investigate which one.)
Cheers,
Dmitriy
PS: Your datatype reminded me of another one, which allows (or allowed)
proving
Hi Makarius,
thanks, this is the hint I was looking for a long time now.
I will do the replacement in the BNF package, but I don't think that I
will have time for it before the approaching release.
Dmitriy
On 07.04.2015 17:47, Makarius wrote:
Just a short note on Local_Theory.open_target
Hi Makarius,
On 10.02.2015 18:30, Makarius wrote:
On Tue, 4 Nov 2014, Makarius wrote:
Strange hacks that work around the absence of proper options encumber
the introduction of them eventually. It is the usual bootstrap
problem for reforms.
I actually did start some work in the vicinity of
Hi Chris,
I've pushed it to the testboard (and will push it to the repository in
case of success):
http://isabelle.in.tum.de/testboard/Isabelle/rev/0d7de4d99eac
Cheers,
Dmitriy
On 28.01.2015 09:55, Christian Sternagel wrote:
It is amazing how easy some things get when a wizard is looking
the changes
to a test server, and push them to the main repo if everything is fine?
cheers
chris
On 11/23/2014 11:42 AM, Dmitriy Traytel wrote:
Hi Christian,
just a few weeks ago, I learned that Envir.subst_term_types is indeed
the wrong function when substituting with a unifier (instead
-functions (and
appropriately plug in ids in the internal BNF constructions)?.
Let me cite the relevant part of my email that you refer to.
On 13.11.2014 15:40, Dmitriy Traytel wrote:
I would not care too much about such dead annotations. If a user made
a variable dead explicitly, she might
On 21.11.2014 15:00, Christian Sternagel wrote:
Hi Dmitriy,
thanks for another round of clarification (I should really reread old
emails before referring to them).
On 11/21/2014 02:43 PM, Dmitriy Traytel wrote:
In general, why not create map-functions that allow to map over *all*
type
Sorry for reviving an ancient thread, but have the constants defined by
inductive ever been visible to find_consts since Florian's commit (I
presume 4a3747517552 ?).
Today in be4a911aca71 (but also in Isabelle2014 and even in
Isabelle2012) in the following
inductive xyz :: bool where xyz
http://isabelle.in.tum.de/reports/Isabelle/report/60d6105dac94411c8f55ea7626a15c71
anybody taking care of this?
Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
This is in Isabelle2014. In 229765cc3414 I make the same measurements as
Larry. So indeed (as the text above those lemmas suggests) there seems
to be a regression with the simplifier setup.
Dmitriy
On 07.11.2014 15:10, Julian Brunner wrote:
The proof that 97 is prime only takes 1.3s on my
hasty to remove
the test which exposed this time leak. Once this issue has been fixed,
I will put the long test back in, with a better comment.
Tobias
On 07/11/2014 15:27, Dmitriy Traytel wrote:
This is in Isabelle2014. In 229765cc3414 I make the same measurements
as Larry.
So indeed
Yes, that's my bad. Thanks! I was about to check Mira for complaints.
See now AFP/ 1dd93cc85dfb.
Dmitriy
On 23.10.2014 14:25, Florian Haftmann wrote:
Isabelle 06dfbfa4b3ea
AFP 33c18a9138e9
*** Unknown old-style datatype Regular_Exp.rexp
*** At command derive (line 18 of
On 17.09.2014 11:40, Jasmin Christian Blanchette wrote:
There are only a handful of old_datatypes left in the AFP, and they will go
away as soon as Dmitriy gets a chance to fix a bug in his code (presumably once he's back
from vacation).
It is now (isabelle/7b92932ffea5) fixed, and the
Hi Chris,
Am 05.09.2014 um 12:27 schrieb Christian Sternagel:
[...]
First question: is this intentional and what is the current default rule?
Yes. Quoting from the news:
The rule set_cases is now registered with the [cases set]
attribute. This can influence the behavior of the cases
Hi René,
this is a tactic failure in the recent size extension (the interface
with fun). We will work on it.
Thanks for the report,
Dmitriy
On 25.06.2014 13:49, René Thiemann wrote:
Dear all,
I have an unexpected problem when defining a datatype using datatype_new.
theory Test
imports
on Derivatives of Regular Expressions
Dmitriy Traytel and Tobias Nipkow
Monadic second-order logic on finite words (MSO) is a decidable yet expressive
logic into which many decision problems can be encoded. Since MSO formulas
correspond to regular languages, equivalence of MSO formulas can be reduced
Am 26.05.2014 11:07, schrieb Jasmin Blanchette:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs.
Am 26.05.2014 11:46, schrieb Tobias Nipkow:
On 26/05/2014 11:07, Jasmin Blanchette wrote:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow nip...@in.tum.de:
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
Am 26.05.2014 12:25, schrieb Makarius:
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The = as the name for Nil's discriminator deserves an explanation.
[...] So I introduced this weird = syntax, which suggests that
equality is used for discriminating. I am open to other suggestions.
Am 26.05.2014 12:53, schrieb Makarius:
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on
options one
could invent long / explicit keywords for them (or Parse.literal
items).
grep gives 371 occurences of -: in IsaFoR's development
Am 13.05.2014 08:09, schrieb Jasmin Christian Blanchette:
Am 12.05.2014 um 23:10 schrieb Makarius makar...@sketis.net:
This sounds both a bit like testing-unstable-HOL. But there is no problem to
experiment with axiomatizations, if it clear to the user what it is, and not a seamingly
Am 12.05.2014 16:54, schrieb Makarius:
This is a continuation of the thread: code_pred introduces axioms?
(October / November 2013).
Back then, on Thu, 31 Oct 2013, Andreas Lochbihler wrote:
When Lukas told me about the axioms about three years ago, he said
that indeed these axioms only
Could it be the document preparation?
Dmitriy
Am 05.05.2014 11:17, schrieb Johannes Hölzl:
Has anybody an idea why the AFP test for Probabilistic_Noninterference
fails?
When I build it on my machine with either the combination in the email
(i.e. AFP acd2cc051b4f and Isabelle 52e5bf245b2a) or
Am 31.03.2014 23:14, schrieb Makarius:
On Fri, 28 Feb 2014, Makarius wrote:
I've made another round of refinements (presently at
Isabelle/f7ceebe2f1b5). There were some situations where the change
propagation of blobs (auxiliary files) versus theories was not right,
leading to an invalid
Am 14.03.2014 13:36, schrieb Makarius:
What is the status of the set_comprehension_pointfree simproc?
In 31afce809794 Dmitriy says set_comprehension_pointfree simproc
causes to many surprises if enabled by default, and in 4d899933a51a
I've tried to reconstruct the missing NEWS entry, since
Hi Makarius,
Am 17.02.2014 14:14, schrieb Makarius:
* Improved support for Isabelle/ML, with jEdit mode isabelle-ml for
auxiliary ML files.
This refers to Isabelle/56ebc4d4d008. It continues recent
improvements of auxiliary file support.
The IDE support for Isabelle/ML is already quite
Am 13.02.2014 12:48, schrieb Makarius:
Today isatest has reported a breakdown of HOL/Library/Code_Prolog.thy.
This was undetected in a more regular test due to this change that
removed it from the normal HOL-Library session:
changeset: 38504:76965c356d2a
user:haftmann
date:
Should be fine again (or at least better) with b445c39cc7e9. Thanks for
the notification.
Dmitriy
Am 12.02.2014 16:28, schrieb Makarius:
Tests about slowness take long, but here is a presumably good point in
the published history:
Isabelle/db691cc79289
Finished Pure (0:00:10 elapsed time,
Am 10.02.2014 14:18, schrieb Makarius:
On Mon, 25 Nov 2013, Dmitriy Traytel wrote:
Am 23.11.2013 19:42, schrieb Makarius:
On Mon, 28 Oct 2013, Dmitriy Traytel wrote:
Concerning the error messages: at least you should always get
strictly more information than without coercion inference
Zorn is supposed to move to Main together with the new (co)datatype
package. I guess it was removed from Library only by mistake.
Dmitriy
Am 26.11.2013 12:58, schrieb Lawrence Paulson:
Of course we don’t have any formal curation policy for the library, but Zorn's
lemma is a fundamental
This refers to Isabelle/d71c2737ee21.
The minimal example is really minimal this time:
theory Scratch
imports Main
begin
end
In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a
moment for the text to turn #EEE3E3, close Main.thy and Scratch.thy is
now outdated as well. The
Am 22.11.2013 21:40, schrieb Makarius:
On Fri, 22 Nov 2013, Dmitriy Traytel wrote:
This refers to Isabelle/d71c2737ee21.
The minimal example is really minimal this time:
theory Scratch
imports Main
begin
end
In Isabelle/jEdit this loads fine. Then Control+click on Main, wait a
moment
From my angle Isabelle/f6ffe53387ef resolves [1] in a robust way. But
I'm waiting for Christian to confirm this.
Dmitriy
Am 21.11.2013 00:13, schrieb René Neumann:
If there will already be a new release, would it perhaps be possible to
merge the fix (given there is a robust one) for this
Am 05.09.2013 13:35, schrieb Florian Haftmann:
I also observed that if you use sledgehammer as old-style keyword, the
proof text is inserted after instead of just replacing
lemma
distinct xs ⟹ n ≠ m ⟹ n length xs ⟹ m length xs ⟹ xs ! n ≠ xs ! m
sledgehammer by (metis distinct_conv_nth)
Am 04.08.2013 18:57, schrieb Florian Haftmann:
For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional nested to mutual reduction to
simulate the old package, so that the same theorems as before are available
(albeit under
Am 25.07.2013 04:16, schrieb Christian Sternagel:
Dear developers,
While the following lemma is proved automatically
lemma converse_subset:
A¯ ⊆ B¯ ⟷ A ⊆ B by auto
I'm not sure exactly how, since simp_trace shows no application of
simplification rules and neither of the rules suggested
, Dmitriy Traytel wrote:
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify
Hi Chris,
I think Variable.polymorphic is what you want to use before using
fastype_of.
Dmitriy
Am 11.07.2013 05:12, schrieb Christian Sternagel:
Dear list,
what is the proper way of obtaining a type from a term, in case I want
to give it as argument to Sign.typ_unify (of Sign.typ_match
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how it
actually used in practice. I just do isabelle build -j4 -a -d
'$AFP' to see immediately how everything works out. It is also
possible to make a quick integrity check via isabelle
Am 15.05.2013 16:34, schrieb Makarius:
On Wed, 15 May 2013, Dmitriy Traytel wrote:
Am 15.05.2013 15:48, schrieb Makarius:
What is still unclear to me after so many years of testboard is how
it actually used in practice. I just do isabelle build -j4 -a -d
'$AFP' to see immediately how
On 24.04.2013 16:18, Brian Huffman wrote:
On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel tray...@in.tum.de wrote:
However, your example is still not printed as expected (assuming that the
output should be equal to the input in this case):
(case x of (a, b) = λ(c, d). e) y
Usually prod_case
Hi all,
since Containers are in the AFP mira results in global crashes of the
build tool
(http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694).
By global I mean that no session is built at all due to an outdated (wrt
Isabelle repository, e.g. 916271d52466)
changes to the handling of
case expressions?
- Brian
On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote:
* Nested case expressions are now translated in a separate check
phase rather than during parsing. The data for case combinators
is separated from the datatype
expressions to work with the new translation check phase?
- Brian
On Wed, Apr 10, 2013 at 9:16 AM, Dmitriy Traytel tray...@in.tum.de wrote:
* Nested case expressions are now translated in a separate check
phase rather than during parsing. The data for case combinators
is separated from
Hi,
theory Scratch
imports Main
begin
term True x
thm TrueI[OF TrueI]
end
behaves very strangely in jedit with Isabelle/5dbe537087aa. For both
commands there is no indication of errors (except of the absence of a
popup). This seams to apply to all Isar commands involving
Hi Clemens,
On 17.03.2013 20:43, Clemens Ballarin wrote:
Dear Developers,
What it the current best practice for testing my change to Isabelle?
There used to be testboard, but I'm unsure how that evolved. Is there
a similar service for testing my change to Isabelle against the AFP?
I do use
I'm looking intro it.
Dmitriy
On 21.12.2012 04:07, Christian Sternagel wrote:
Dear all,
just now, when I tried
hg in
in the development repo, I got the error below. My mercurial version
is 2.2.3 (for at least some weeks). Did anybody else experience
similar problems?
cheers
chris
No one knows if somebody is doing something wrong.
I did a fresh clone (from the topmost non corrupted changeset) once
again. Few commits are missing (I think by Jasmin and Sascha), as I
didn't have them locally. You are both welcome to repush through
lxbroy10 (please avoid macbroy20-29).
On 17.12.2012 15:23, Makarius wrote:
On Thu, 13 Dec 2012, Dmitriy Traytel wrote:
I use Mercurial 2.2 and after pushing ed6b40d15d1c the attached error
log was generated. hg verify on the server says that c4a27ab89c9b is
the first damaged changeset. The corrupted repository is still
The test run was ok, but the repository is corrupted once again. Trying
to repair by stripping.
Dmitriy
On 13.12.2012 13:23, Dmitriy Traytel wrote:
It worked for me. I'm currently building (or more precisely running
the build tool ;-) ) and will push if it succeeds.
Dmitriy
On 13.12.2012
).
Dmitriy
On 13.12.2012 13:58, Dmitriy Traytel wrote:
The test run was ok, but the repository is corrupted once again.
Trying to repair by stripping.
Dmitriy
On 13.12.2012 13:23, Dmitriy Traytel wrote:
It worked for me. I'm currently building (or more precisely running
the build tool
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
Hi all,
On 19.08.2011 01:38, Gerwin Klein wrote:
Should we ask a wider audience (isabelle-users) if anybody else has
good reasons against/for a change?
Another small advantage of set as an own datatype arises in the context
of subtyping.
We use map functions to lift coercions between base
84 matches
Mail list logo