Hi all,
If you have installed Kodkodi for Nitpick and have update Isabelle in
the last couple of minutes or so, you might eventually notice that
Nitpick doesn't work anymore. There are two solutions to this problem:
1. Download http://www4.in.tum.de/~blanchet/kodkodi-1.2.4.tgz and edit
Hi,
Tobias asked me to look at Sledgehammer and see if it would be
possible to improve the relevance filter and the proof reconstruction
to get a better success rate. As a first step towards that, I was
thinking of refactoring the Sledgehammer code. In particular:
1. Put all the
Hi Makarius,
Am 13.01.2010 um 17:57 schrieb Makarius:
The ATP manager is relatively new (and clean),
I have to disagree here -- but not with the new part. I find it
dubious that ATP_Manager is based on ATP_Wrapper and not the other way
around. As a result, adding a new ATP (besides E,
Hi all,
I was trying to make Nitpick more context-friendly and thought that
local_setup and Generic_Data would be my friends. However, local_setup
seems to do nothing -- the changes I perform to the data are coldly ignored.
The little theory below shows illustrates what I mean:
theory
Hi all,
Last week I experienced strange errors on my machine regarding mkdir on my
Mac (with Nitpick and Sledgehammer), but these eventually went away after I
pulled a newer version of Isabelle.
Now I'm testing on macbroy2 and getting similar errors, but this time in
Imperative HOL:
***
Am 01.10.2010 um 17:03 schrieb Makarius:
On Fri, 1 Oct 2010, Jasmin Blanchette wrote:
[...]
Has anybody run into similar issues before?
Yes, it merely means there is an inconsistency between the sources (notably
lib/scripts/process) and the compiled image. You merely need to make sure
Hi all,
Last week I attended LPAR-17 (Int'l Conf. on Logic for Programming,
Artificial Intelligence and Reasoning) and IWIL-2010 (Int'l Workshop
on the Implementation of Logics) in Yogyakarta, Indonesia. The LPAR
proceedings are in my office; those for IWIL are online at
Hi Kishanthan,
Thanks for your interest!
I'm interested in working with isabelle for this google summer of code.
I have gone through the ideas list of Isabelle and i'm interested in
working on A general proof representation framework.
To be honest i'm fairly new to isabelle. So i would like
Am 21.06.2011 um 23:11 schrieb Clemens Ballarin:
After updating my Isabelle repository (which I haven't done for
quite a while) Poly/ML stopped to start up. I have 5.2 and
according to the release notes this is no longer supported. Do I
need to build 5.4 for myself or do we provide a
Hi all,
Isar generally lets users refer to unnamed local facts using the backtick
notation. For example,
lemma hd [x] = x
using hd.simps[where xs = []]
thm `!!x. hd [x] = x`
works fine. However, the same mechanism doesn't understand unfolding:
definition null xs = (xs =
Hi Makarius,
The 'unfolding' element refers to the dynamic state, so there is no way to
refert to such hidden results later. The notation for literal facts `...` is
even more restrictive in limiting the scope to the visible part of the
context, i.e. things that are produced in the proof
Hi Alex,
It works for me (tested with Isabelle2011) when I replace null with
List.null (There is a hide_const (open) in List.thy). Otherwise the
unfolding doesn't actually unfold anything :-)
You're right, it works, also with the latest Isabelle. I don't know what I
tested this morning,
Hi Makarius,
I have also thought again about 'unfolding' as such: it might actually
qualify as preserving textual structure and thus as something that can be
included in the textual scope for `...` -- assuming it will someday really
cease to perform arbitrary simplification by accident.
Hi all,
Somewhere between 43ca06e6c168 and 6975db7fd6f0, I seem to have broken the AFP
entry Lam-ml-Normalization. However, I cannot reproduce the problem on my
machine -- whether in Proof General nor using isabelle make.
On the other hand, I do get the following disturbing messages in Proof
Hi Makarius,
Am 17.11.2011 um 12:12 schrieb Makarius:
This is merely a consequence of
changeset: 45486:600682331b79
user:wenzelm
date:Mon Nov 14 16:16:49 2011 +0100
files: src/Pure/Isar/runtime.ML
description:
more detailed exception_trace: in Poly/ML 5.4.x
Hi Makarius,
Good question. There is a brief explanation at
http://hgbook.red-bean.com/read/mercurial-in-daily-use.html
in the section Divergent renames and merging.
Did it produce any merge node locally? What does hg out say?
lapbroy152:HOL blanchet$ hg out
Vergleiche mit
Am 01.12.2011 um 13:06 schrieb Stefan Berghofer:
I just got the very same warnings when updating my copy of the Isabelle
sources. I already got similar warning messages
warning: detected divergent renames of
src/HOL/Tools/Sledgehammer/sledgehammer.ML to:
Hi all,
The automatic prover SPASS, integrated in Sledgehammer, now includes many
enhancements, such as properly oriented term simplification, that should make a
difference for Isabelle problems. Thanks to these, SPASS has become more
effective than E, Vampire, or Z3 [1], and this is just the
Am 24.04.2012 um 17:21 schrieb Makarius:
I did not dare to enable overlord mode so far, but doing it on your behalf it
reveals the follow in prob_e_1_proof:
/cygdrive/c/Users/wenzelm/Desktop/Isabelle_23-Apr-2012/contrib/e-1.4/x86-cygwin/eproof:
line 24:
Hi Makarius,
I suppose here that the self-extracting Isabelle_23-Apr-2012.exe archive did
extract correctly, to something like 850 MB directory structure?
At least it had the expected directory structure.
Your existing Cygwin is probably relatively old, such that the poly.exe
cannot be
Am 24.04.2012 um 20:58 schrieb Makarius:
have also made some more experiments. The Empty exception is from the
split_last here
http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614
where you don't get any output unexpectedly,
Am 19.07.2012 um 12:49 schrieb Sascha Boehme:
I don't know for sure. It might be that YICES_INSTALLED and friends were
added as a sanity check to avoid errors when invoking the solver locally and
it doesn't exist. If that's the case, it's probably better to remove
YICES_INSTALLED and just
Hi all,
In the new codatatype package, which we aim at integrating into Isabelle soon,
there are 1277 @{thm} annotations spread over about 10 000 lines of ML. On my
machine, each @{thm} costs about 30 ms, which means that 40 s of CPU time is
spent alone looking up theorems whenever we load or
Am 10.08.2012 um 20:02 schrieb Makarius:
30ms for the conjuring trick with fully abstract @{thm} is odd, it should not
happen. Can you spend some time to figure out the time hole?
The delta between @{thm} and @{fasthm} is really just a couple of lines of code:
val i = serial ();
Am 10.08.2012 um 22:21 schrieb Makarius:
On Fri, 10 Aug 2012, Jasmin Blanchette wrote:
I'm attaching my test files for the record. Dmitriy tried these already and
confirmed my measurements.
OK, I will also look for the fat.
The slowdown is neither in put_thms nor the_thm(s
Am 10.08.2012 um 23:43 schrieb Makarius:
On Fri, 10 Aug 2012, Jasmin Blanchette wrote:
The slowdown is neither in put_thms nor the_thm(s), but apparently
rather in the compiler somehow. The ML code in ml appears to be executed
two orders of magnitude slower than normal ML code
Am 11.08.2012 um 23:44 schrieb Makarius:
On Fri, 10 Aug 2012, Jasmin Blanchette wrote:
Now, here's something really strange. If I replace
fun thm_bind kind a i =
val ^ a ^ = the_ ^ kind ^
(ML_Context.the_local_context ()) ^ string_of_int i ^ ;\n;
with
fun my_ctxt
Hi all,
I am trying to get the JDK 1.7 using the command
isabelle components -a
but the command returns immediately. The diagnosis command
isabelle components -l
prints
Available components:
/Users/blanchet/isabelle
/Users/blanchet/isabelle/src/Tools/Code
Hi Makarius,
There is still something missing, as far as I can tell from your components
-l printout before.
You need to init components from the Admin/components/* space explicitly to
claim them, and the let components -a resolve them. The general attitude
is to provide various parts
Am 03.12.2012 um 23:08 schrieb Lawrence Paulson:
Missing components maybe?
I did isabelle components -a earlier today. In fact, the issue is likely to
be related to the big upgrade that resulted from my invocation of this very
command yesterday night.
Jasmin
Am 04.12.2012 um 07:51 schrieb Lars Noschinski:
Did you try starting jEdit with -f to force a fresh build?
That did the trick. Thanks!
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Am 04.12.2012 um 15:06 schrieb Makarius:
If you provide a state where the SMT_Examples session can reproduce its
proofs,
I'll try to. Last time I regenerated the certificate, there were a couple of
cases where I was not successful with 3.2 (on my Mac) and had to use 4.0. But I
need to dig
Am 04.12.2012 um 15:29 schrieb Makarius:
The question which SMT/Z3 version to ship with the release basically has time
until the new year.
I'm a big fan of if it ain't broken don't fix it, so let's defaut on 3.2, and
in the unlikely event that both the parser issue with 4.0 and rewr_conv are
Am 04.12.2012 um 18:11 schrieb Johannes Hölzl:
I remove the SMT certificates in HOL-Multivariate_Analysis in
Isabelle/4b4fe0d5ee22.
Thanks! I didn't mean to apply pressure on you, though. ;)
Jasmin
___
isabelle-dev mailing list
Am 08.12.2012 um 14:07 schrieb Makarius:
In your observations above, are you sure that nondeterministically means
physical nondeterminism, say due to parallel loading of theories? Or
theories that you have visited before in Proof General, before starting the
above one?
Each time I
Am 10.12.2012 um 15:28 schrieb Makarius:
See also this old thread:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03001.html
Interesting. Unfortunately, I get the same errors with macbroy20, 21, 22, 23...
Jasmin
___
Am 01.01.2013 um 14:29 schrieb Makarius:
Testing it briefly myself, it works except for SMT_Word_Examples:
Solver z3: Z3 proof parser (line 2): unknown sort: bv
Could you give me some details about how/where this occurs exactly? The
SMT_Word_Examples.thy file starts with
declare
Am 01.01.2013 um 22:38 schrieb Makarius:
Anyway, since the smt method seems to work right now, I propose to wire up
a test where smt_certificates and smt_read_only_certificates are left
unchanged if ISABELLE_FULL_TEST is enabled. Does that make sense, according
to the meaning of these
is
incomplete with respect to Joe Hurd's Metis, even though the prover has only
six simple well-documented proof rules.) Incompleteness can strike any time.
Anfang der weitergeleiteten E-Mail:
Von: Jasmin Blanchette jasmin.blanche...@gmail.com
Datum: 29. Oktober 2012 13:11:49 MEZ
An: Sascha
Hi Makarius,
Change cb5cdbb645cd (clarified bootstrapping of Pure) altered the semantics of
Multithreading.max_threads_value ()
with Poly/ML. Namely, all of a sudden the function returns 1 instead of 4 on a
4-CPU machine, which seems strage as a default for a function called
Hi all,
I just updated Isabelle to af8ecf09a58c (from a version that was one or two
days old) and whenever I try to build HOL, I get this error:
isabelle build -c -b HOL
Fehler: Hauptklasse isabelle.Build konnte nicht gefunden oder geladen werden
0:00:00 elapsed time, 0:00:00 cpu
Am 01.08.2013 um 18:15 schrieb Makarius makar...@sketis.net:
Another important missing piece is primcorec.
What is the proper technical term for that? Isn't it just corec?
If the proper name for primrec is primrec, then the proper name for this is
primcorec.
I wouldn't mind killing the
Hi Florian,
Am 04.08.2013 um 18:57 schrieb Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de:
has an explicit need for a »nested to mutual« mode ever been
articulated?
Yes, on a couple of occasions. First, as Dmitriy mentioned, compatibility is
important -- I certainly don't want
Hi Florian,
An example could be something like
primitive_recursion card :: 'a set = nat
where
card {} = 0
card (insert x A) = Suc (card A)
proof -
show !!x y. insert x o insert y = insert y o insert x
show !!x. insert x o insert x = insert x
qed
thm card.simps -- {*
card {} =
Hi Alex,
- The package registers a datatype interpretation to generate congruence
rules the case combinator for each type.
I guess it would make sense to have the package do that, or is there a specific
reason why it is better to do it in a function-related extension?
- The pattern
Am 13.09.2013 um 09:34 schrieb Lawrence Paulson l...@cam.ac.uk:
None of them work.
Can you reproduce it in Proof General?
As an additional test, you could try playing with options like debug and see
if the output says anything interesting.
Just to make sure it's not MaSh-related somehow, I
Hi Makarius,
This looks really bad, and needs to be investigated further. I've not seen
such a bad visual drop-out in the past 1-2 years, despite many minor mistakes
in the painting of Java on many different platforms.
I might be also responsible myself, potentially doing some text
Am 18.09.2013 um 16:51 schrieb Makarius makar...@sketis.net:
OK, just a few more details: The jEdit Global Options / Text Area pane has
various tuning parameters that affect the font style. What are your
preferences for the following?
Anti Aliased smooth text
Fractional font metrics
Hi Larry,
Am 13.09.2013 um 21:17 schrieb Lawrence Paulson l...@cam.ac.uk:
That fixed it.
One of the Australians has run into the same issue with MaSh. The issue should
be addressed starting with Isabelle/8d9f4e89d8c8. If you're willing to give
MaSh a second try, you could try to set MASH=yes
Am 24.09.2013 um 22:10 schrieb Makarius makar...@sketis.net:
OK, I will tell you when we are getting close to the fork point.
Thanks. We'll try to maintain the ready to be forked invariant, but it's
always good to have advance notice, if nothing else so that we avoid bigger
changes right
Am 25.09.2013 um 13:03 schrieb Makarius makar...@sketis.net:
On Wed, 25 Sep 2013, Jasmin Christian Blanchette wrote:
Isabelle/jEdit is currently unwilling to process theories
The file is correctly opened, but nothing is processed -- no imports are
processed, the theory text has a pink
Hi Alex,
(Briefly reviving an old thread...)
Am 06.08.2013 um 00:36 schrieb Alexander Krauss kra...@in.tum.de:
In summary, except for the size functions which are somewhat special
(and only used for termination proofs), the function package never uses
any inductiveness and would happily
Hi Makarius,
Am 20.11.2013 um 14:12 schrieb Makarius makar...@sketis.net:
Dmitriy had sent me some explanations which sessions represent the material
to be moved to HOL in either case, but I never tried it out myself. It is
high time to do that now. In particularly I would like to get a
Am 20.11.2013 um 17:17 schrieb Makarius makar...@sketis.net:
We have a bad state in Isabelle/d983a020489d:
* HOL-BNF_Example fails like this:
*** Theory loader: failed to load Gram_Lang (unresolved DTree)
*** Theory loader: failed to load Parallel (unresolved DTree)
*** Extra variables
Am 26.11.2013 um 13:01 schrieb Dmitriy Traytel tray...@in.tum.de:
Zorn is supposed to move to Main together with the new (co)datatype package.
I guess it was removed from Library only by mistake.
Yes, it should definitely be in Library for now. My change 483131676087 took it
out by mistake.
Am 22.01.2014 um 21:18 schrieb Makarius makar...@sketis.net:
On Tue, 21 Jan 2014, Jasmin Christian Blanchette wrote:
This brings the new (co)datatype package where we want it to be for the next
release.
Great. This is a big step forward.
Thank you for your kind words.
I would like to
Hi Larry,
Am 23.01.2014 um 14:38 schrieb Lawrence Paulson l...@cam.ac.uk:
Great news! I hope to see a brief announcement paper illustrating some of the
new things that can be done. Or did you publish that last year?
I believe you are on the committee of a conference where such a paper has
Am 12.02.2014 um 20:40 schrieb Makarius makar...@sketis.net:
Mainly the proof reconstruction on the Isabelle side, especially the question
of type variables.
I can't help much there. Perhaps Larry knows more. All I can recall is that
Metis sometimes suggests type instantiations (since types
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice of
names in Skolemization, that has been entirely redone in the past few years.
I imagine it is now something like this:
Subgoal.FOCUS (fn
Hi Andreas,
I read the comment to your changeset 3def821deb70, which says that Nat.pred
may show up in theorems generated by primcorec. This is fine, because the
destructor view for codatatypes goes well with discriminators and selectors
for datatypes. As I do not know where discriminators
Hi Makarius,
While experimenting with the increasingly useful Isabelle/ML IDE, I've found
various spots that are awaiting further cleanup, renovation or demolition.
Just some arbitrary examples:
* HOL/SAT.thy with some related ML modules. I've brushed this up
recently, e.g. to get
Hi Andreas,
Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler
andreas.lochbih...@inf.ethz.ch:
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to
depend on it, and (please correct me if I'm mistaken) hardly anybody go
Hi Andreas,
How big an issue is it to you if we move narrowing to Library?
[...] If you do so, please make sure that the connection to the datatype
packages is kept, i.e., narrowing generators are generated for all datatypes
(even those that are defined while narrowing was not in scope).
Hi Larry,
Am 15.03.2014 um 16:27 schrieb Lawrence Paulson l...@cam.ac.uk:
But working very well, in my experience.
I'm glad to hear that. :)
Now, will smt2 calls be suitable for the Library and AFP?
No, because they suffer from the exact same issues as smt calls. We could of
course rethink
Hi Andreas,
4. If anybody has any ideas on how to address Scenario 3, please let me
know!
I don't think that scenario 3 is the one to address. IMO the hooks should
behave as if they were executed in the name space of the datatype
declaration, so size is doing something sensible already.
For the record: The AFP was apparently never down. It's just my ISP at home
that doesn't seem to like sourceforge.net these days. Even basic things like
ping don't work from home -- but they do work when I'm logged on a TU server.
Strange...
Jasmin
Am 23.04.2014 um 07:35 schrieb Tobias Nipkow
Am 13.05.2014 um 15:35 schrieb Makarius makar...@sketis.net:
On Tue, 13 May 2014, Dmitriy Traytel wrote:
Let me explain Jasmin's ;): bnf_axiomatization was the name, I intended
for the command first, before I was persuaded by my colleagues to correlate
the name with typedecl rather than
Am 25.05.2014 um 14:59 schrieb Makarius makar...@sketis.net:
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
In the course of a day, I typically find myself pulling from the Isabelle
repository several times. I am encouraged in this by my use of Mercurial
queues. So it's not
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. set
rel_list vs. forall_list2
un_Cons1 vs. hd
Am 26.05.2014 um 12:25 schrieb Makarius makar...@sketis.net:
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
Am 26.05.2014 um 12:05 schrieb Makarius makar...@sketis.net:
The observed here problem is different: the type constructor list somehow
ends up in the name space with a concealed flag. There might be one or
more Binding.conceal too many in the BNF sources.
Ah, now I get it. Of course this
Am 26.05.2014 um 15:24 schrieb Makarius makar...@sketis.net:
I think you could afford an actual keyword for the dead modifier and use it
without colon, like lazy in HOLCF/domain. That would substract dead from
the normal identifier space, but merely means its very few occurrences on
Hi Chris,
Just a reminder that this old thread is not yet resolved and currently I'm
essentially stuck.
I hope somebody who has a clue will answer your email.
Independent of my being stuck, could one of the devs apply at least the first
of the following attached patches (and the second
Hi all,
When editing inside Isabelle/jEdit (f19f4afa49e2), it used to be so that
everything above was left alone. Now, if I edit a lemma in the middle of the
window, everything above it that is visible gets reprocessed. So if I write
something like
thm list.exhaust
it can take a couple of
On 26.03.2015, at 14:00, Peter Lammich lamm...@in.tum.de wrote:
Isabelle version: devel -- hg id 034b13f4efae
Someone pushed a fix a few hours ago already (75433c3ee203).
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Hi Gerwin,
Thanks for that pointer. FOL-Fitting looks reasonably well behaved with its
2-way nesting. This file has 4-way nesting and something seems to have
changed in the order of the subgoals that the induction leaves, which makes
the unstructured apply scripts a pain to update.
Is
What is still not clear to me is how provers are determined. The
Sledgehammer panel uses the system option sledgehammer_provers, after many
failed attempts in the past to cope with the ML heuristics. In
Isabelle/323feed18a92 I've tried to update this wrt. recent changes. Is it
true
Hi Gerwin,
From your first email:
I’m still seeing a different order of premises in the rules themselves,
though. Maybe that only occurs for more than 2 constructors, or it has to do
with the fact that my case is not just mutual through one set of datatypes,
but also involves a third
Does it really fully unregister?
Not fully: (I believe) it unregisters only the non-nested occurrences, e.g. “a”
and “b” in my previous example (several emails ago). For “a list” and “b list”,
there is some hope, since the old package used to do it right (keeping them
apart from the fully
Hi Gerwin,
On 19.04.2015, at 16:45, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
The datatype manual says in e8472fc02fe5:
The datatype_compat command is needed to register new-style datatypes for
use with fun and function (Section 2.2.2)
Is this still correct?
Indeed, this is a
Hi Gerwin,
The rule set I’d need is “typ_desc_typ_struct.inducts”, which datatype_compat
doesn’t generate. It does generate the four constituent rules that I can put
in a set myself, but the order of premises in these rules is different to the
old datatype package, which means my goal
The rule set I’d need is “typ_desc_typ_struct.inducts”, which
datatype_compat doesn’t generate.
The rule you’re looking for is called “compat_a_b_a_list_b_list.induct” (no
s).
Actually, it’s the other way around. With the old package, the “inducts” rule
is just a collection of four
Hi Gerwin,
On 19.04.2015, at 20:25, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
Thanks for updating.
Currently trying to pull through proofs in
https://github.com/seL4/l4v/blob/master/tools/c-parser/umm_heap/CTypes.thy
They are unfortunately pretty horrid to start with (violating
Hi Andreas,
In Isabelle2014, processing this datatype declaration takes about one minute.
So what has happened in between? (The Isabelle2014 timing panel is also way
off with 8 seconds.)
Thanks for your report. What happened in between is that we generate more
theorems. I suspect one or a
Can you explain the status of Old_SMT? Is there anything that isatest still
needs to run here?
“old_smt” is there just in case. I was thinking of killing it right after the
Isabelle2015 release. It’s not even tested by any regression test. People like
Filip Maric, who use Z3 heavily (cf.
Hi Florian,
a) The radical solution: there is only »_ / _« for both field division
and euclidean division. How natural is notation like »a / b * b + a mod
b = a« then?
b) The conservative solution: partial division has »_ div _«, an (the
more special) field division »_ / _«. This seems more
Makarius wrote:
* Convenience: users somethings find it too combersome to type proper
Isabelle symbols.
I never do that myself, but take the time to type things nicely. It
is actually not much time for me, since I implemented the input
methods myself and know how they work.
Concerning :: versus \Colon I am in favour to get rid of \Colon
altogether: there is visually no difference in final LaTeX documents, and in
the editor it introduces a bit too much complication to my taste.
As far as I am concerned: By all means, kill it!
At some point in 2014, I realized
I suspect they have updated Vampire and the new version’s proof format has
changed a bit. I have it on my TODO list.
Jasmin
On 18.07.2015, at 23:37, Jason Dagit dag...@gmail.com wrote:
On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson l...@cam.ac.uk
mailto:l...@cam.ac.uk wrote:
I’ve seen
Hi Makarius,
> My impression is that ebf296fe88d7 (blanchet) causes HOL-Proofs to run out of
> resources and fail. I've made approx. 3 runs in the vicinity -- it always
> takes very long.
>
> Is that another failure to do a full "isabelle build -a" before pushing
> anything?
I did "isabelle
> On 06.10.2015, at 22:37, Makarius wrote:
>
>> On Tue, 6 Oct 2015, Dmitriy Traytel wrote:
>>
>> So the main candidates for bad changesets are: ebf296fe88d7, 2ebdd603cd71.
>
> More results on macbroy2:
>
> 5b5656a63bd6
> Finished HOL-Proofs (0:18:14 elapsed time, 0:49:28
Thanks, sorry (24b5e7579fdd).
Jasmin
> On 06.10.2015, at 11:42, Dmitriy Traytel wrote:
>
> The title says it all.
>
> Dmitriy
___
isabelle-dev mailing list
isabelle-...@in.tum.de
Hi Florian, Frédéric,
Sorry for not answering this earlier. Somehow, I failed to notice that two of
the three functions are my responsibility.
>> During some programming tasks, I had to use the following functions:
>>
>> BNF_FP_Def_Sugar.co_datatype_cmd
>
> note that these *_cmd functions are
> On 18.11.2015, at 16:26, Lawrence Paulson wrote:
>
> These suggestions are worth a discussion. Should we go ahead? Would anybody
> like to apply this patch and test that everything still works?
I could do it, if nobody has objections.
Jasmin
Dear Burkhart,
> in Isabelle 2016, certain traditional interfaces to data-type packages
> do no longer exist, for example Datatype.get_info thy typename or
> its homologue on records. This function yielded for a given typename
> the list of constructors together with their types, and other
> What is special about Sudoku?
You're right, probably nothing.
>> SMT_Tests (requires Z3)
> ...
> In 2013 we did not have Z3 as default component, usable for everybody. Now
> the condition on it is always true -- z3 is always enabled.
We could indeed enable it by default.
>> Slow:
>> Brackin
Hi Lars,
> However, turns out that the actual problem was that somebody pushed
> something completely unrelated (maybe a different repository?) into
> testboard. This also generated a gargantuan changelog in Jenkins. I
> don't blame that person, it could happen to anyone. But we need to fix
>
> but this leads to the rather lengthy "insert_mset x M" as opposed to the
> current "{#x#} + M". This would come up in all inductive proofs. If we want
> to mimic sets, it actually seems unavoidable...
With completion, it might actually be easier to type "insert_mset x M" than
"{#x#} + M".
> The problem is a missing macro \textsubscript
Thanks for the heads-up. I added the "subscript" package, which is supposed to
help (d0fc75798baf); then I reverted that and gave up the idea of having bold
subscripts (19387866eace), since there was another issue with \textsubscript
(spurious
Hi Makarius,
You wrote:
> Mixfix annotations have gained a more formal status recently, with PIDE
> markup reports that lead to some highlighting and tooltips in the IDE.
> [...]
> BNF datatypes are a notable exception. E.g. this example produces duplicate
> "bad" markup about Unicode in
1 - 100 of 113 matches
Mail list logo