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

[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 some cardinality material. When 
we moved the BNF package into Main, I surgically split the HOL-Cardinals 
theories into two, moving the exact dependencies into Main and leaving the rest 
outside. As a result, it's pretty random what's in Main and what's outside. The 
alternative -- moving all of HOL-Cardinals into Main -- seemed undesirable 
because it would slow down building Main quite a bit.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Vampire

[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 documentational purpose. If the default were 
"no" instead, many noncommercial users would likely fail to enable Vampire.

I'm not married to the above scheme, but the years of experience with it and Z3 
(until Z3 was open-sourced) suggest that it works well.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Vampire

[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 course spaces should be ignored, esp. at the end.

I just copied old code I inherited from Sascha Böhm and his Vampire 
noncommercial. For sure there are endlessly many ways in which we could make 
Isabelle and Sledgehammer more user friendly. In Qt/C++, we had a 
"stripWhiteSpace" function that would do the trick. But string manipulation in 
ML is like pulling teeth. If you happen to know which function I can call, I'll 
gladly change the code.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Vampire

[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 simple as a typo or a spurious space? The only 
recognized values are "yes" and "no" (upper- or lowercase). What happens if you 
change the option to "no"? What happens if you change it back to "yes"?

Could you send me the contents of your file "~/.isabelle/etc/preferences"?

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

  |> Variable.add_fixes (mk_names n "s")

Dmitriy, since this is your code, could you take a look at it? The line in 
question seems to have been added as part of an optimization you did in 2016 
(see 8053ef5a0174).

Cheers,

Jasmin

> On 31. May 2018, at 10:28, Lars Hupel  wrote:
> 
> since approximately Isabelle/e0cd57aeb60c (~1 week):
> 
> *** Malformed global fact
> "Misc_N2M.linorder_class.f1_t.n2m_t_ctor_fold_dict"
> *** Illegal fixed variable: "s1"
> *** At command "primrec" (line 164 of
> "~~/src/Benchmarks/Datatype_Benchmark/Misc_N2M.thy")
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 starting every sentence with "I think" or "I 
believe", since obviously whatever I say is my opinion, but since this 
apparently leads to confusion, I'll happily relativize my previous statement: 
Just as you found one style more readable than another (without giving any 
evidence), *I* find

foo ==>
bar

and especially

foo ==> bar ==>
baz

much more readable than the alternative, because they yield less opportunities 
for what Bryan Garner (Modern Am. E. Usage) refers to as "miscues" when 
parsing. When I read the alternative, I get the same effect as when I listen to 
the Murder City Devils and they sing

God knows she's pretty
messed up

I don't think there's a need for a big empirical study to observe the miscue; 
it should be easily reproducible by any left-to-right reader. By the same 
token, I can understand that in the presence of [| ... |], the opposite 
convention has its benefits (as stressed by Andreas).

One more case: Suppose you have

foo ==>
bar ==> baz

Notice how the break falls naturally where you would insert the parentheses:

foo ==>
(bar ==> baz)

Compare with

foo ==> (bar
==> baz)

So I will be apologized, surely, for preferring the end-of-line treatment for 
operators that bind to the right, while realizing that I might be in the 
minority on this mailing list.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 operator names on the next line improves readability,
> independent of what the operator is. However, unless there is significant
> support, I won't press for a uniform change.

Short version: I would generally support such a change if it excludes operators 
that bind to the right, especially => and ==>.

Long version: My impression is that people like to have "boring" operators on 
the right and "interesting" ones on the left. Boring operators include "=" on 
lists, conjunction for logical formulas, cons and append for lists, and + for 
numbers. Oh, I was about to forget the absolutely most boring operator of all: 
commas in lists. There's a reason why commas on the left look so revolting 
(even if the convention has some advantages).

If you're playing with lists or strings, then # and @ will tend to be boring 
operators, and something like

"blah blah blah " @ my_file_name @
" blah blah"

will feel quite natural; there's usually no need to draw attention to the @. 
Ditto for commas in lists.

In logic, often conjunction is a boring connective, but one could argue that 
there is no "default" connective (logic being so subtle) and they should all be 
displayed prominently, on the left, Lamport-style (possibly without the leading 
bullet-like conjunction on the first line), to prevent any misreadings.

However, for operators like ==>, which bind on the right,

foo ==>
bar

is actually much more readable than

foo
==> bar

When reading the first line, "foo ==>", we immediately see that something is 
missing, and that "foo" has negative polarity. In the second version, "foo" 
looks positive, until one reads "==> bar". Things get even worse when you have 
either

foo ==> bar ==>
baz

which is good, or

foo ==> bar
==> baz

which really looks like "foo implies bar" until you keep reading.

> - The issue of multiple line breaks in the current unparsing of long formulas
> like _ + _ + _ + _ + _ + _ is independent and very annoying. I would be
> surprised if we wanted anything but fill every line, not just the first or 
> last
> one as happens right now. A solution of that one would be much appreciated.

I agree.

> - I also noticed that "=" is still at the end of the line while "<=" and
> friends are at the beginning. That is indeed inconsistent, also with
> traditional notation. I agree with Larry and am strongly in favour of
> changing that.

This might be an instance of the boring vs. non-boring phenomenon. There is, I 
guess, a strong tradition for the statu quo, but were it to be changed, then 
"=" should be the one that goes on the left. Given that "=" is used perhaps 10 
times more often than "<=" and friends, this could turn out to be more 
distracting than the current inconsistency.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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?
> 
> At the moment I somewhat prefer "linked" (or maybe "linked_by") since
> sortedness implies that "P" is some kind of order, which it doesn't have
> to be.

It also reminds me of my "derivation" predicate, which arose when formalizing 
Bachmair & Ganzinger's chapter in the Handbook of Automated Reasoning:

https://bitbucket.org/isafol/isafol/src/f0f585fb6cbd7097567cc1c493fe1b3c1223a8da/Bachmair_Ganzinger/Proving_Process.thy?at=master=file-view-default

It's a bit different because of the use of lazy lists (to allow infinite 
derivations) and the different handling of the empty list.

Underlying all of these appears to be the concept of a "chain". That's what we 
often call things of the form x1 > x2 > ... > xn (finite) or x1 > x2 > ... 
(infinite), where > is some binary relation. In the context of Bachmair & 
Ganzinger, or, indeed, for formalzing Definition 7.2.3 from Baader & Nipkow, it 
makes sense to use a relation > that is not transitive.

So maybe "chain" could be a good name for the finite concept?

Incidentally, Georges Gonthier believes that for nonempty paths in a graph (or 
more generally chains), the first element should be stored separately from the 
other ones. I guess the main benefit is when concatenating two paths, he can 
simply append. I'm not sure how relevant it is to us, though.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 code and doesn't slow up building Main 
noticeably), but we're also working on the "nunchaku" component itself, which 
we will repack and update. We'll also add an "smbc" component, for another 
OCaml tool also developed by Simon Cruanes [*], which provides a "SAT solver + 
narrowing" backend to the "nunchaku" tool.

I will also update the "Nitpick_Examples" to also perform regression tests on 
Nunchaku.

I'm aiming at doing all the necessary changes by the end of August at the 
latest.

Jasmin

[*] https://cedeela.fr/~simon/files/cade_17_paper.pdf

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 infrastructure, which often ignored some 
> commits.

The same applies to me (VU Amsterdam), and I believe Mathias Fleury (MPII 
Saarbrücken) is also a heavy user of Testboard when he modifies Isabelle (e.g. 
the multiset library).

From a pure basic user's perspective, I don't see much of a difference between 
Mira and Jenkins. To me it's just Testboard, and most of the time it works, and 
then I'm happy. Sometimes Mathias just sends me a link to a patch he's pushed 
to Testboard for me to review, before he pushes it to Isabelle. That's also 
very useful.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 me debug it.

> In current Isabelle/6acb28e5ba41 it is also possible to use something
> like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space
> to the requirements of MY_SESSION.

Good to know.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

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

/Users/blanchette/isabelle/src/Tools/jEdit/dist/jars/Isabelle-jEdit.jar:
Cannot start: 
*** No such file: 
"/Users/blanchette/isabelle/src/HOL/Library/Fraction_Field.thy"
*** The error(s) above occurred for theory "HOL-Lib.Fraction_Field" (line 17 of 
"/Users/blanchette/hgs/isafor/thys/ROOT")
*** No such file: 
"/Users/blanchette/isabelle/src/HOL/Library/Fundamental_Theorem_Algebra.thy"
*** The error(s) above occurred for theory 
"HOL-Lib.Fundamental_Theorem_Algebra" (line 18 of 
"/Users/blanchette/hgs/isafor/thys/ROOT")
*** No such file: 
"/Users/blanchette/isabelle/src/HOL/Library/Polynomial_Factorial.thy"
*** The error(s) above occurred for theory "HOL-Lib.Polynomial_Factorial" (line 
29 of "/Users/blanchette/hgs/isafor/thys/ROOT")
*** The error(s) above occurred in session "HOL-Lib" (line 1 of 
"/Users/blanchette/hgs/isafor/thys/ROOT")

But then I can't use Isabelle/jEdit. I was better off 2 days ago. Back then, 
things worked.

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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

I just pulled and updated (f533820e7248) before carrying out any further tests. 
Now I get the same error as Jenkins:

$ isabelle build -b HOL
*** No such file: "/Users/blanchette/isabelle/src/HOL/Main.thy"
*** The error(s) above occurred for theory "Main" (line 8 of 
"/Users/blanchette/isabelle/src/HOL/ROOT")
*** The error(s) above occurred in session "HOL" (line 3 of 
"/Users/blanchette/isabelle/src/HOL/ROOT")

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 => 
>> p._2.exists(_.theory == "Main"))
>>   ^
> 
> You need to do this in the Console plugin of Isabelle/jEdit, switched
> into Scala mode.

I see. It prints

res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] = None

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 == "Main"))
>> 
>> Maybe the Scala build state is not clean? (I couldn't find how to clean it 
>> in the system manual.)
> 
> A forced build of everything works like this:
> 
>  isabelle jedit -bf

It doesn't help:

$ isabelle jedit -bf
### Building Isabelle/Scala ...
### Building Isabelle/jEdit ...

$ isabelle scala
Welcome to Scala 2.11.8 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_121).
Type in expressions for evaluation. Or try :help.

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 => 
p._2.exists(_.theory == "Main"))
   ^

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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 system with Isabelle 
for over two years now. I also have a Sierra laptop at work, which I can test 
on Monday.

> What is your $ISABELLE_HOME actually?

$ isabelle getenv ISABELLE_HOME
ISABELLE_HOME=/Users/blanchette/isabelle

> Is there anything special with the underlying file-system?

Not that I am aware of.

> Here is an example for the Console/Scala toplevel within Isabelle/jEdit:
> 
> scala> PIDE.resources.session_base.known.files.toList.find(p =>
> p._2.exists(_.theory == "Main"))
> res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] =
> Some((/home/makarius/isabelle/repos/src/HOL/Main.thy,List(Main)))
> 
> What is your result?

:12: error: not found: value PIDE
   PIDE.resources.session_base.known.files.toList.find(p => 
p._2.exists(_.theory == "Main"))

Maybe the Scala build state is not clean? (I couldn't find how to clean it in 
the system manual.)

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Bitbucket SSH craziness escalates

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

In your ~/isabelle/afp/devel/.hg/hgrc, I presume there's a line that looks like 
this:

default = https://bitbucket.org/isa-afp/afp-devel

Change it to

default = ssh://h...@bitbucket.org/isa-afp/afp-devel

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev