Re: [isabelle-dev] Bitbucket SSH craziness escalates

> 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 >

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

>> 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"

> 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"

> 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"

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] Bad theory import "Main"

> 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"

> 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] Uses of Jenkins at TUM

> 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] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy

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

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] Bad theory import "Main"

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] ~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy broken

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 -> ()

> 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 -> ()

> 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] Vampire

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

> 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] Vampire

> 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] [Spam] cardinality primitives in Isabelle/HOL?

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