Re: [isabelle-dev] [Spam] cardinality primitives in Isabelle/HOL?

2019-01-23 Thread Blanchette, J.C.
Hi Larry, You wrote: > The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so > clearly a lot of facts about cardinals are available already in Main. FYI: As you might already know or deduced from the name convention, the (co)datatype (a.k.a. "BNF") package is based on

Re: [isabelle-dev] Vampire

2018-07-04 Thread Blanchette, J.C.
Makarius wrote: > I don't remember the reason for its "tristate logic", with "unknown" as > default. The thinking is as follows. In an "unknown" state, "vampire" gets added to the list of provers by Sledgehammer, and users get a warning. In a "no" state, it doesn't. Thus, "unknown" serves a

Re: [isabelle-dev] Vampire

2018-07-04 Thread Blanchette, J.C.
> I’m at home today so don’t have access to that file. Please send it to me once you have a chance. > But even if I somehow misspelt “yes” five times, But maybe you wrote "true" five times? > would it revert to “unknown”? Any value other than "yes" and "no" is taken as "unknown". > Of

Re: [isabelle-dev] Vampire

2018-07-04 Thread Blanchette, J.C.
> On 3 Jul 2018, at 13:07, Lawrence Paulson wrote: > > I keep getting the error message below. I have changed this option many times > but it never sticks. It has been happening consistently since yesterday. > > ~/isabelle/Repos/src/HOL: hg id > ec4fe1032b6e tip Could it be something as

Re: [isabelle-dev] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

2018-05-31 Thread Blanchette, J.C.
Hi Lars, Thanks for the heads-up. Makarius's change e0cd57aeb60c is clearly the immediate source of the problem, but the more profound cause seems to be some nonstandard handling of variables. The "illegal fixed variable" in question, "s1", seems to originate from line 397 in "bnf_fp_n2m.ML":

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Blanchette, J.C.
> This sort of claim needs to be justified by evidence. We had it the first way > until the late 1990s. I changed it to the other way while working on large > proof states connected with crypto protocols. It seemed more readable to me > for such proofs. I was taught at school to avoid

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Blanchette, J.C.
> On 11 Jan 2018, at 16:44, Tobias Nipkow wrote: > > There are a number of different points here. > > - What is good style depends on what your math look like. Knuth writes nice > traditional math, whereas Isabelle proof states can get quite ugly. In such > cases I find that

Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

2017-08-16 Thread Blanchette, J.C.
Hi Christian, Tobias, > I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my > "linked" from the AFP (Efficient_Mergesort). > > > https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html > > Maybe we could unify the constants/names somehow? > >

Re: [isabelle-dev] The coming release of Isabelle2017

2017-07-06 Thread Blanchette, J.C.
Hi Makarius, > Is there anything else to take into account for this late-summer release > process? Simon Cruanes (cc:) and I are still working on Nunchaku, which we intend to become Nitpick's successor. I have some patches locally that move the current "Nunchaku.thy" to Main (it's not much

Re: [isabelle-dev] Uses of Jenkins at TUM

2017-04-24 Thread Blanchette, J.C.
> On 24 Apr 2017, at 17:12, Andreas Lochbihler > wrote: > > Sure. Whenever I have to push something to the Isabelle repository, I use the > Jenkins testboard installation to see whether something broke. It works more > reliably than the previous testboard

Re: [isabelle-dev] Bad theory import "Main"

2017-04-24 Thread Blanchette, J.C.
Hi Makarius, > The problem is in the HOL-Lib session from isafor. It is somewhere in > your ROOTS (or -d specifications). Ah! > Are you working with IsaFoR on purpose, or is this just an accident? That's it. I had IsaFoR as a component -- half on purpose, half by accident. Thanks for helping

Re: [isabelle-dev] Bad theory import "Main"

2017-04-23 Thread Blanchette, J.C.
> This means you should see some "Java vomit" on the terminal at startup > of Isabelle/jEdit, as well as some text popup with a half-decent error > message. Plugin startup is always a bit fragile. Yes, it does both I guess. The "half-decent error message" looks like this:

Re: [isabelle-dev] Bad theory import "Main"

2017-04-23 Thread Blanchette, J.C.
>> I see. It prints >> >> res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] = None > > There is probably something wrong with the general session layout. The > critical changeset shows an old fallback to Pure: > http://isabelle.in.tum.de/repos/isabelle/rev/ae09b9f5980b#l4.10

Re: [isabelle-dev] Bad theory import "Main"

2017-04-22 Thread Blanchette, J.C.
> On 22.04.2017, at 19:17, Makarius wrote: > >> scala> PIDE.resources.session_base.known.files.toList.find(p => >> p._2.exists(_.theory == "Main")) >> :12: error: not found: value PIDE >> PIDE.resources.session_base.known.files.toList.find(p => >>

Re: [isabelle-dev] Bad theory import "Main"

2017-04-22 Thread Blanchette, J.C.
> On 22.04.2017, at 17:24, Makarius <makar...@sketis.net> wrote: > > On 22/04/17 13:26, Blanchette, J.C. wrote: >> >> :12: error: not found: value PIDE >> PIDE.resources.session_base.known.files.toList.find(p => >> p._2.exists(_.theory == &

Re: [isabelle-dev] Bad theory import "Main"

2017-04-22 Thread Blanchette, J.C.
> Odd. I cannot reproduce this on Linux or macOS Sierra. It didn't happen to me yesterday night either, even though I was using the same changeset. It just started this morning when I restarted Isabelle/jEdit, for no apparent reason. I'm using El Capitan on this laptop. I've been using this

Re: [isabelle-dev] Bad theory import "Main"

2017-04-22 Thread Blanchette, J.C.
Hi again, I wrote: > Something strange is happening with the repository (as per > Isabelle/701bb74c5f97). I nailed it down to change ae09b9f5980b. Before that change, Main is loaded normally. With this change, I get the error Bad theory import "Main" Jasmin

Re: [isabelle-dev] Bitbucket SSH craziness escalates

2017-02-21 Thread Blanchette, J.C.
> On 21.02.2017, at 22:12, Lawrence Paulson wrote: > > I committed some changes (fixing AFP-devel), which I would like to push. But > what in God’s name is this? > > ~/isabelle/afp/devel/thys: hg push > pushing to https://bitbucket.org/isa-afp/afp-devel >