[isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)

[Lawrence Paulson]

Does anybody know what this is?

01:58:19 Running HOL-Quickcheck_Benchmark ...01:58:20 HOL-Quickcheck_Benchmark: 
theory HOL-Quickcheck_Benchmark.Needham_Schroeder_Base01:58:20 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Find_Unused_Assms_Examples01:58:23 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Guided_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_No_Attacker_Example01:58:24 
HOL-Quickcheck_Benchmark: theory 
HOL-Quickcheck_Benchmark.Needham_Schroeder_Unguided_Attacker_Example02:12:01 
Warning - Unable to increase stack - interrupting thread02:12:01 *** 
Interrupt02:12:01 HOL-Quickcheck_Benchmark FAILED

Larry

> Begin forwarded message:
> 
> From: Isabelle/Jenkins 
> Subject: [Isabelle-ci] Build failure in Isabelle (benchmark)
> Date: 12 March 2019 at 01:22:32 GMT
> To: isabelle...@mail46.informatik.tu-muenchen.de
> 
> The Isabelle build failed. See the log at: 
> https://ci.isabelle.systems/jenkins/job/isabelle-nightly-benchmark/887/

build.log
Description: Binary data
> ___
> Isabelle-ci mailing list
> isabelle...@mail46.informatik.tu-muenchen.de
> https://mailman46.informatik.tu-muenchen.de/mailman/listinfo/isabelle-ci

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

Re: [isabelle-dev] Current AFP problems

[Lawrence Paulson]

I’m getting no alerts for some reason 
Larry

> On 8 Mar 2019, at 19:23, Florian Haftmann 
>  wrote:
> 
> isabelle: 03bc14eab432 tip
> afp: 16e89cda027a tip

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

[isabelle-dev] Redundant definitions in Analysis

[Lawrence Paulson]

In Analysis, we have two equivalent definitions of continuous functions between 
two topological spaces:

lemma "continuous_map X Y f = continuous_on_topo X Y f"
  by (auto simp add: continuous_map_def continuous_on_topo_def vimage_def 
image_def Collect_conj_eq inf_commute)

The first one comes from HOL Light and is defined in Abstract_Topology. The 
latter is declared in Function_Topology.

Obviously we need to eliminate one of them, and I prefer the former name. The 
latter is more logical but clunky, especially when compound with others in 
theorem names.

Any comments?

Larry

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

Re: [isabelle-dev] infix line breaking

[Lawrence Paulson]

I’d be in favour!
Larry

> On 23 Feb 2019, at 15:07, Makarius  wrote:
> 
> It might be better to introduce a proof-local version of 'abbreviation'.

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

Re: [isabelle-dev] infix line breaking

[Lawrence Paulson]

Which reminds me: I define such abbreviations all the time, using “let”. Could 
let-abbreviations be folded upon printing?

Larry

> On 23 Feb 2019, at 09:10, Manuel Eberl  wrote:
> 
> I for one almost always do
> 
>   define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
> 
> in such cases, perhaps occasionally combined with a
> 
>   note [simp] = G_def [symmetric]
> 
> at least during the "exploratory" stage of Isar proof writing.
> 
> Without that, statements and proof obligations in HOL-Algebra become
> totally unreadable in my experience.
> 
> Manuel
> 
> 
> On 22/02/2019 17:20, Lawrence Paulson wrote:
>> The pretty printing of infix operators looks pretty terrible in the presence 
>> of large terms.
>> 
>> I’d like to propose having infix operators breaking at the start of the line 
>> rather than at the end. Any thoughts?
>> 
>> Larry
>> 
>> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) 
>> {pp}) {} (nsphere 0) {} r
>>   d =
>>hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 
>> 0) {nn}) {} r
>>   (inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
>> ___
>> 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

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

Re: [isabelle-dev] infix line breaking

[Lawrence Paulson]

The point is the line breaking. Look at the occurrence of d before the =. This 
applies to all infix operators, not just relations.
Larry

> On 22 Feb 2019, at 17:10, Tobias Nipkow  wrote:
> 
> We had already discussed this and decided that for "=", "<=" etc it makes 
> sense.
> 
> I find that the wrong associativity can be much more of a killer than where 
> the infix op is placed.
> 
> Tobias
> 
> On 22/02/2019 17:20, Lawrence Paulson wrote:
>> The pretty printing of infix operators looks pretty terrible in the presence 
>> of large terms.
>> I’d like to propose having infix operators breaking at the start of the line 
>> rather than at the end. Any thoughts?
>> Larry
>> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) 
>> {pp}) {} (nsphere 0) {} r
>>d =
>> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>>  (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 
>> 0) {nn}) {} r
>>(inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
>> ___
>> 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

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

[isabelle-dev] infix line breaking

[Lawrence Paulson]

The pretty printing of infix operators looks pretty terrible in the presence of 
large terms.

I’d like to propose having infix operators breaking at the start of the line 
rather than at the end. Any thoughts?

Larry

inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) {pp}) 
{} (nsphere 0) {} r
   d =
hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
 (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) 
{nn}) {} r
   (inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Analysis not building

[Lawrence Paulson]

This worked — thanks!
Larry

> On 2 Feb 2019, at 13:56, Makarius  wrote:
> 
> Can you try the following in your $ISABELLE_HOME_USER/etc/settings?
> 
>  init_component "$HOME/.isabelle/contrib/polyml-test-1b2dcf8f5202"
> 
> Apparently, the last two updates on polyml-test were not as monotonic as
> I was hoping, despite clear improvements by David Matthews.

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

Re: [isabelle-dev] Analysis not building

[Lawrence Paulson]

It died twice using “isabelle jedit -l HOL-Analysis”, once using "isabelle 
jedit Analysis/Analysis.thy” and once using "isabelle build -b HOL-Analysis”.

The reason I fetched in the first place was that I was getting crashes in my 
interactive sessions.

Larry

> On 2 Feb 2019, at 13:26, Florian Haftmann 
>  wrote:
> 
>> HOL-Analysis can’t be built (reproducibly) with the latest version 
>> (76f2d492627e). It simply dies, no error message.
> 
> I cannot reproduce this.
> 
>  ML_PLATFORM="x86_64_32-linux"
>  ML_SYSTEM="polyml-5.7.1"
>  ML_OPTIONS="--maxheap 9G"
> 
> Have you tried a fresh build or delete the corresponding log / saved
> state manually?
> 
> Cheers,
>   Florian
> 

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

[isabelle-dev] Analysis not building

[Lawrence Paulson]

HOL-Analysis can’t be built (reproducibly) with the latest version 
(76f2d492627e). It simply dies, no error message.

Larry

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

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

[Lawrence Paulson]

Last January 24, I moved Fpow into Main and introduced 
Library/Equipollence.thy. Hope you like it.

Larry

> On 26 Jan 2019, at 15:14, Andrei Popescu  wrote:
> 
> Sorry for my late reply. I agree it makes sense to move such basic operators 
> (and facts) into Main. The Ordinals and Cardinals development was "destined" 
> to this sort of exports from the very beginning.
> 
> Best wishes, 

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

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

[Lawrence Paulson]

This makes perfect sense to me.

I suggest moving at least the definition of Fpow into Main (it’s small, and 
fundamental) while creating a new Library entry for my own new material.

Larry

> On 23 Jan 2019, at 12:48, Blanchette, J.C.  wrote:
> 
> 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] cardinality primitives in Isabelle/HOL?

[Lawrence Paulson]

The question of dependency is tricky. I tried deleting the reference to 
HOL-Cardinals.Cardinals and found that most of the elementary results were 
easily provable using other library facts. But then there was this:

lemma lepoll_trans1 [trans]: "⟦A ≈ B; B ≲ C⟧ ⟹ A ≲ C"
  by (meson card_of_ordLeq eqpoll_iff_card_of_ordIso lepoll_def lepoll_trans 
ordIso_iff_ordLeq)

The theorem ordIso_iff_ordLeq is proved in BNF_Wellorder_Constructions, so 
clearly a lot of facts about cardinals are available already in Main.

But I do prove a couple of things involving the operator Fpow:

lemma lepoll_restricted_funspace:
   "{f. f ` A ⊆ B ∧ {x. f x ≠ k x} ⊆ A ∧ finite {x. f x ≠ k x}} ≲ Fpow (A × B)"
proof -
  have *: "∃U ∈ Fpow (A × B). f = (λx. if ∃y. (x, y) ∈ U then SOME y. (x,y) ∈ U 
else k x)"
if "f ` A ⊆ B" "{x. f x ≠ k x} ⊆ A" "finite {x. f x ≠ k x}" for f
apply (rule_tac x="(λx. (x, f x)) ` {x. f x ≠ k x}" in bexI)
using that by (auto simp: image_def Fpow_def)
  show ?thesis
apply (rule subset_image_lepoll [where f = "λU x. if ∃y. (x,y) ∈ U then @y. 
(x,y) ∈ U else k x"])
using * by (auto simp: image_def)
qed

lemma eqpoll_Fpow:
  assumes "infinite A" shows "Fpow A ≈ A”

The thing is though, Fpow (which is nothing but the finite powerset operator) 
probably belongs in Main as well.

An alternative proposal is to create a new theory, Library/Equipollence. I 
agree about hiding the syntax.

Larry

> On 23 Jan 2019, at 10:11, Traytel Dmitriy  wrote:
> 
> Hi Larry,
> 
> if you want to put the definitions and the basic properties in Main, then 
> Fun.thy would probably be the place. But then I would argue that the syntax 
> should be hidden, as users might want to use these symbols for something else.
> 
> For the advanced material, do you need some theorems from HOL-Cardinals or 
> just the syntax from HOL-Library.Cardinal_Notations in addition to what is 
> already there in Main about cardinals? If it is only the syntax, then a 
> separate theory in HOL-Library is probably a good fit. Otherwise, a separate 
> theory in HOL-Cardinals would make sense.
> 
> Dmitriy

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

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

[Lawrence Paulson]

I’m trying to install some of my new material and I’m wondering what to do with 
equipollence and related concepts:

definition eqpoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≈" 50)
  where "eqpoll A B ≡ ∃f. bij_betw f A B"

definition lepoll :: "'a set ⇒ 'b set ⇒ bool" (infixl "≲" 50)
  where "lepoll A B ≡ ∃f. inj_on f A ∧ f ` A ⊆ B"

definition lesspoll :: "'a set ⇒ 'b set ⇒ bool" (infixl ‹≺› 50) 
  where "A ≺ B == A ≲ B ∧ ~(A ≈ B)"

The raw definitions are extremely simple and could even be installed in the 
main Isabelle/HOL distribution. The basic properties of these concepts require 
few requisites. However, more advanced material requires the Cardinals 
development. 

Where do people think these definitions and proofs should be installed?

Larry

> On 27 Dec 2018, at 20:29, Makarius  wrote:
> 
> On 27/12/2018 17:45, Traytel  Dmitriy wrote:
>> Hi Larry,
>> 
>> the HOL-Cardinals library might be just right for the purpose:
>> 
>> theory Scratch
>>  imports "HOL-Cardinals.Cardinals"
>> begin
>> 
>> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"
>>  by (rule card_of_ordLeq[symmetric])
>> 
>> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)"
>>  by (rule card_of_ordIso[symmetric])
>> 
>> lemma
>>  assumes "|A| ≤o |B|" "|B| ≤o |A|"
>>  shows "|A| =o |B|"
>>  by (simp only: assms ordIso_iff_ordLeq)
>> 
>> end
>> 
>> The canonical entry point for the library is the above 
>> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in 
>> Main, because the (co)datatype package is based on them. The syntax is 
>> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations 
>> (which HOL-Cardinals.Cardinals does transitively).
> 
> It would be great to see this all consolidated and somehow unified, i.e.
> some standard notation in Main as proposed by Larry (potentially as
> bundles as proposed by Florian), and avoidance of too much no_syntax
> remove non-standard notation from Main.
> 
> 
>   Makarius

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

Re: [isabelle-dev] Poly/ML x86_64_32 available for testing

[Lawrence Paulson]

Looks impressive. Thanks!
Larry

> On 22 Jan 2019, at 11:27, Makarius  wrote:
> 
> Here are some performance measurements on the best hardware that I have
> presently access to (not at TUM):

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

Re: [isabelle-dev] mercurial accident

[Lawrence Paulson]

Sorry, I’m to blame for this. When Angeliki mentioned she had merge conflicts, 
it turned out she didn’t have diffmerge (or anything similar) on her machine. 
By the time I got everything configured and managed to resolve the conflicts 
(largely by discarding her work unfortunately), I unthinkingly pushed the 
result without testing.

Larry


> On 18 Jan 2019, at 10:42, Lars Hupel  wrote:
> 
>> The problem behind this: Angeliki got administrative push-access to the
>> Isabelle repository, without anybody at Cambridge showing her how to use it.
> 
> Before we start blaming individual people, this is not a person problem,
> but a tooling problem. Industry has figured out this problem years ago.
> One doesn't simply allow pushes to master (or "default" in Mercurial).
> CakeML has adopted this too.
> ___
> 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] cardinality primitives in Isabelle/HOL?

[Lawrence Paulson]

Tons of useful stuff here.

Some syntactic ambiguities, particularly around the =o relation, which is also 
defined as Set_Algebras.elt_set_eq.

I don’t suppose there’s any chance of using quotients to define actual 
cardinals and use ordinary equality? And it still makes sense to introduce the 
actual notion of equipollence and similar relations.

Larry

> On 27 Dec 2018, at 20:29, Makarius  wrote:
> 
> On 27/12/2018 17:45, Traytel  Dmitriy wrote:
>> Hi Larry,
>> 
>> the HOL-Cardinals library might be just right for the purpose:
>> 
>> theory Scratch
>>  imports "HOL-Cardinals.Cardinals"
>> begin
>> 
>> lemma "|A| ≤o |B| ⟷ (∃f. inj_on f A ∧ f ` A ⊆ B)"
>>  by (rule card_of_ordLeq[symmetric])
>> 
>> lemma "|A| =o |B| ⟷ (∃f. bij_betw f A B)"
>>  by (rule card_of_ordIso[symmetric])
>> 
>> lemma
>>  assumes "|A| ≤o |B|" "|B| ≤o |A|"
>>  shows "|A| =o |B|"
>>  by (simp only: assms ordIso_iff_ordLeq)
>> 
>> end
>> 
>> The canonical entry point for the library is the above 
>> HOL-Cardinals.Cardinals. Many of the theorems and definitions are already in 
>> Main, because the (co)datatype package is based on them. The syntax is 
>> hidden in main—one gets it by importing HOL-Library.Cardinal_Notations 
>> (which HOL-Cardinals.Cardinals does transitively).
> 
> It would be great to see this all consolidated and somehow unified, i.e.
> some standard notation in Main as proposed by Larry (potentially as
> bundles as proposed by Florian), and avoidance of too much no_syntax
> remove non-standard notation from Main.
> 
> 
>   Makarius

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

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

[Lawrence Paulson]

> On 27 Dec 2018, at 12:45, Florian Haftmann 
>  wrote:
> 
> (I don't know how useful the strict versions less_poll, greater_poll
> would be).

Strict versions do turn up in some places (both in HOL Light and Isabelle/ZF)

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

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

[Lawrence Paulson]

> On 27 Dec 2018, at 12:39, Florian Haftmann 
>  wrote:

Thanks for the suggestions.

> The input abbreviation gepoll should be added as well.
> 
> Anyway, I am uncertain about the name »poll«.

From https://en.wikipedia.org/wiki/Cardinality

"Two sets A and B have the same cardinality if there exists a bijection from A 
to B, that is, a function from A to B that is both injective and surjective. 
Such sets are said to be equipotent, equipollent, or equinumerous. This 
relationship can also be denoted A ≈ B or A ~ B.”

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

[isabelle-dev] illegal reflective access

[Lawrence Paulson]

Got this upon launch. Is it important?

341ebf35464b tip

Larry

/Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/classes
/Users/lp15/isabelle/Repos/src/Tools/jEdit/dist
/Users/lp15/isabelle/Repos/src/Tools/jEdit/dist/classes
WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by macosx.MacOSXPlugin to method 
com.apple.eawt.FullScreenUtilities.setWindowCanFullScreen(java.awt.Window,boolean)
WARNING: Please consider reporting this to the maintainers of 
macosx.MacOSXPlugin
WARNING: Use --illegal-access=warn to enable warnings of further illegal 
reflective access operations
WARNING: All illegal access operations will be denied in a future release

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

Re: [isabelle-dev] Remaining uses of {* ... *} quotation?

[Lawrence Paulson]

> On 8 Nov 2018, at 20:32, Makarius  wrote:
> 
> In particular, what are the remaining uses of {* ... *}?

I didn’t even know that existed.

But I use (*...*) to enclose arbitrary text or comment material out.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Lemma "sum_image_le"

[Lawrence Paulson]

Sounds good to me!
Larry

> On 28 Sep 2018, at 14:00, Alexander Maletzky  
> wrote:
> 
> 
> lemma "sum_image_le" in theory "Groups_Big", which is stated for
> type-class "ordered_ab_group_add", holds more generally for
> "ordered_comm_monoid_add" (proof below). May I propose to change it
> accordingly?
> 
> Best regards,
> Alexander

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

Re: [isabelle-dev] Frag / Poly_Mapping

[Lawrence Paulson]

It seems there is clearly a need for something of the sort to go into 
HOL/Library. Maybe it could be completely independent of Poly_Mapping, and the 
latter perhaps could be rewritten in terms of it.

Now who is volunteering to do this? I could certainly rewrite my "Frag.thy" to 
use the material I sent out yesterday and make independent of Poly_Mapping, but 
would that meet everyone's needs?

Larry

> On 25 Sep 2018, at 06:18, Akihisa Yamada  
> wrote:
> 
> Dear Alexander, Florian, Larry, Manuel,
> 
> recently I also made the same typedef, so that derivatives can be defined, 
> which wants real norm in current Isabelle/HOL. Unfortunately I didn't notice 
> it is called "poly_mapping".
> 
> I propose calling them finsupp or finite_supp. Support is often written 
> "supp", and the term in this meaning is clearly about functions so I don't 
> think "_fun" is needed.
> 
> Best regards,
> Akihisa

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

Re: [isabelle-dev] Frag / Poly_Mapping

[Lawrence Paulson]

> On 24 Sep 2018, at 10:30, Alexander Maletzky  
> wrote:
> 
> Some notions defined in "Frag.thy" already exist in "Poly_Mapping.thy": 
> "support" is called "keys" there, and I think "frag_cmul" could easily be 
> defined in terms of "map".
> 
> "frag_extend" looks like a special case of a more general subsitution 
> homomorphism "subst" of type "('a => 'b => 'c) => ('a =>_0 'b) => 'c", 
> defined as "subst f x = (\Sum i\in keys x. f i (lookup x i))", which could 
> indeed be added to "Poly_Mapping.thy". The insertion morphism in 
> "MPoly_Type.thy" could then perhaps be defined in terms of "subst" (at least 
> partially; for power-products, the above sum would have to be replaced by a 
> product).

Thanks for that. Manuel is expressing the opposite point of view, namely that 
it might be better to keep the two developments 100% separate. Certainly the 
basic setup of Frag is simple and short (see below) and we don't have to 
concern ourselves with how Poly_Mapping is used by other developments in the 
AFP and in other projects outside. So I'm puzzled as to the best course.

Larry

typedef 'a frag = "{f::'a\int. finite {x. f x \ 0}}"
  by (rule exI [where x = "\x. 0"]) auto

definition support 
  where "support F = {a. Rep_frag F a \ 0}"

declare Rep_frag_inverse [simp] Abs_frag_inverse [simp]


instantiation frag :: (type)comm_monoid_add
begin

definition zero_frag_def: "0 \ Abs_frag (\x. 0)"

definition add_frag_def: "a+b \ Abs_frag (\x. Rep_frag a x + 
Rep_frag b x)"

lemma finite_add_nonzero: "finite {x. Rep_frag a x + Rep_frag b x \ 0}"
proof -
  have "finite {x. Rep_frag a x \ 0}" "finite {x. Rep_frag b x \ 
0}"
using Rep_frag by auto
  moreover have "{x. Rep_frag a x + Rep_frag b x \ 0} \ {x. 
Rep_frag a x \ 0} \ {x. Rep_frag b x \ 0}"
by auto
  ultimately show ?thesis
using infinite_super by blast
qed

lemma finite_minus_nonzero: "finite {x. - Rep_frag a x \ 0}"
  using Rep_frag [of a] by simp

instance 
proof
  fix a b c :: "'a frag"
  show "a + b + c = a + (b + c)"
by (simp add: add_frag_def finite_add_nonzero add.assoc)
next
  fix a b :: "'a frag"
  show "a + b = b + a"
by (simp add: add_frag_def add.commute)
next
  fix a :: "'a frag"
  show "0 + a = a"
by (simp add: add_frag_def zero_frag_def)
qed

end

instantiation frag :: (type)ab_group_add
begin

definition minus_frag_def: "-a \ Abs_frag (\x. - Rep_frag a x)"

definition diff_frag_def: "a-b \ a + - (b::'a frag)"

instance 
proof
  fix a :: "'a frag"
  show "- a + a = 0"
using finite_minus_nonzero [of a]
by (simp add: minus_frag_def add_frag_def zero_frag_def)
qed (simp add: diff_frag_def)

end


definition frag_of where "frag_of c = Abs_frag (\a. if a = c then 1 
else 0)"

lemma frag_of_nonzero [simp]: "frag_of a \ 0"
proof -
  have "(\x. if x = a then 1 else 0) \ (\x. 0::int)"
by (auto simp: fun_eq_iff)
  then have "Rep_frag (Abs_frag (\aa. if aa = a then 1 else 0)) 
\ Rep_frag (Abs_frag (\x. 0))"
by simp
  then show ?thesis
unfolding zero_frag_def frag_of_def Rep_frag_inject .
qed

definition frag_cmul :: "int \ 'a frag \ 'a frag"
  where "frag_cmul c a = Abs_frag (\x. c * Rep_frag a x)"


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

[isabelle-dev] Frag / Poly_Mapping

[Lawrence Paulson]

Attached is a port of the HOL Light “frag” library (free Abelian groups) built 
upon Poly_Mapping. It’s a mess, especially with the combination of frag and 
Poly_Mapping names. Some of it clearly could be added to Poly_Mapping, maybe 
all of it. But it needs to be rationalised. 

Comments / advice?

Larry



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

Re: [isabelle-dev] Explorer.thy [was: performance problems]

[Lawrence Paulson]

I regard it as indispensable. But it does need better pretty printing. Also I 
greatly prefer the if/for format to assume/fix.

Larry

> On 12 Sep 2018, at 07:23, Florian Haftmann 
>  wrote:
> 
>>> On 7 Sep 2018, at 19:18, Makarius  wrote:
>>> 
>>> I can't try it out, since theory "Explorer" is missing.
>> 
>> Attached. A very cool thing.
> 
> Nice to see that old draft from 5 years ago.
> 
> I would still agree that such a tool would be tremendously useful, but
> before going into the distro it would need technical improvement, i.e.
> more civilized approach toward Isar proof text generation, similar to
> Sledgehammer_Isar_Proof.
> 
> Any opinions on that?
> 
> Cheers,
>   Florian
> 
> --
> 
> PGP available:
> http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] performance problems

[Lawrence Paulson]

> On 7 Sep 2018, at 19:18, Makarius  wrote:
> 
> I can't try it out, since theory "Explorer" is missing.

Attached. A very cool thing. 


Explorer.thy
Description: Binary data


> For 16 GB, I usually run Poly/ML in 32-bit mode

How do you do that?

Larry

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

Re: [isabelle-dev] performance problems

[Lawrence Paulson]

What do you suggest for these on a 16 GB machine? I attach my file.
Larry


On 7 Sep 2018, at 15:01, Makarius  wrote:If you are using the 64-bit version of Poly/ML, you should give both--minheap and --maxheap, otherwise it tends to overcommit a lot of memory.

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

[isabelle-dev] performance problems

[Lawrence Paulson]

I'm facing serious performance problems with the development version and I have 
no idea what's happening, though it may be connected with my settings. At the 
moment I am using

JEDIT_JAVA_OPTIONS64="-Xms2048m -Xmx8192m -Xss8m"
ML_OPTIONS="--minheap 3500"

(I'm not aware of any guidelines of what sort of settings are appropriate.)

My theory doesn't use the AFP and I have moved aside my components file, which 
refers to afp/devel. My theory imports nothing but Complex_Main. Yet still, 
Isabelle/jEdit takes on the order of a minute to launch, and freezes (with 
permanent pink markup) within 5 – 20 minutes of launching. My machine has 12 
virtual cores and 16 GB of memory. What could I be doing wrong?

In case it's relevant
~/isabelle/Repos/src/HOL: hg id
58bf801d679a tip


Larry

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Lawrence Paulson]

This trace doesn’t tell us much because it’s only blast’s internal search. 
Looks like every “continuous_on” goal is immediately solved. But after this 
search exits, the reconstructed Isabelle proof will fail. Blast will re-enter 
but it will only find these unsound proofs, and probably won’t ever terminate.
Larry

> On 2 Sep 2018, at 15:00, Manuel Eberl  wrote:
> 
> Okay I did some more experiments and I was now, interestingly enough,
> completely unable to reproduce the situation where Green /didn't/
> timeout. So I have no idea what was going on there; perhaps I made a
> mistake in testing it. I don't know.
> 
> It might be wise to remove "continuous_on_discrete" etc. from
> intro/continuous_intros and declare it as a simp rule instead. I'm still
> not quite sure what causes these problems. I attached a log of blast
> with "blast_trace" enabled.
> 
> Manuel
> 
> On 01/09/2018 14:20, Makarius wrote:
>> This thread consists of two sub-threads. The hardware / OS question
>> still needs to be sorted out: it might be something with Arch Linux.
>> 
>> Apart from that, my reading of blast.ML is that the "continuous_on" rule
>> is applied in the search independently of its fine-grained type
>> information. Is that correct?
>> 
>> 
>>  Makarius
>> 
>> 
>> On 01/09/18 13:19, Lawrence Paulson wrote:
>>> Surely the main issue that blast somehow behaves differently depending upon 
>>> which machine it’s running on?
>>> 
>>> Larry
>>> 
>>>> On 31 Aug 2018, at 22:35, Makarius  wrote:
>>>> 
>>>> On 31/08/18 22:00, Manuel Eberl wrote:
>>>>> That's interesting. I suspected one of the "continuous_on" rules would
>>>>> be the cause. In any case, I don't know how the unification works
>>>>> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
>>>>> apply to this goal at all due to its restrictive type class constraint.
>>>> Blast does its own unification, without taking fully account of types
>>>> and type classes. The found proof is then reconstructed as in "fast" and
>>>> its friends, using regular Isabelle term + type unification.
>>>> 
>>>> Larry should be able to say more precisely, what the limits of blast are.
> 

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Lawrence Paulson]

It’s important to understand that blast knows nothing about type classes. This 
isn’t a problem for rules like order_trans, where the type class constraint 
would be satisfied in most cases. But it’s fatal for continuous_on_discrete: it 
will succeed in all cases, but if the type class constraint isn’t satisfied 
(and it usually won’t be), then the proof will fail and it’s not clear that 
backtracking will find an alternative. The PROOF FAILED message (if it still 
exists) alerts us to this.

Larry

> On 1 Sep 2018, at 13:39, Manuel Eberl  wrote:
> 
>> This thread consists of two sub-threads. The hardware / OS question
>> still needs to be sorted out: it might be something with Arch Linux.
> 
> I don't really have much of an opportunity to test this on other systems
> atm, but I'll see what I can do.
> 
>> Apart from that, my reading of blast.ML is that the "continuous_on" rule
>> is applied in the search independently of its fine-grained type
>> information. Is that correct?
> 
> Even if it is, it has no preconditions, so I don't see how it could
> cause nontermination.
> 
> Manuel

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

Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Lawrence Paulson]

Surely the main issue that blast somehow behaves differently depending upon 
which machine it’s running on?

Larry

> On 31 Aug 2018, at 22:35, Makarius  wrote:
> 
> On 31/08/18 22:00, Manuel Eberl wrote:
>> That's interesting. I suspected one of the "continuous_on" rules would
>> be the cause. In any case, I don't know how the unification works
>> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
>> apply to this goal at all due to its restrictive type class constraint.
> 
> Blast does its own unification, without taking fully account of types
> and type classes. The found proof is then reconstructed as in "fast" and
> its friends, using regular Isabelle term + type unification.
> 
> Larry should be able to say more precisely, what the limits of blast are.
> 
> 
>   Makarius

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

Re: [isabelle-dev] Vampire

[Lawrence Paulson]

> On 4 Jul 2018, at 11:11, Blanchette, J.C.  wrote:
> 
>> I’m at home today so don’t have access to that file.
> 
> Please send it to me once you have a chance.

It seems that I did finally succeed in getting the option set. My guess is that 
the Mac app doesn't necessarily save settings, depending on whether you exit 
with Isabelle > Quit Isabelle or File > Exit. And I’m not sure which one of 
these is supposed to work.

> But even if I somehow misspelt “yes” five times,
> 
> But maybe you wrote "true" five times?

certainly not.

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

Re: [isabelle-dev] Vampire

[Lawrence Paulson]

Well, there’s this:

> String.translate (fn c => if Char.isSpace c then "" else str c) " y   e   s  
> ";
val it = "yes": string

No idea what Isabelle/ML does to these primitives however.

Larry

> On 4 Jul 2018, at 11:11, Blanchette, J.C.  wrote:
> 
> 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.

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

[isabelle-dev] Vampire

[Lawrence Paulson]

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

Larry

"vampire": Error: The Vampire prover is not activated; to activate it, set the 
Isabelle system option "vampire_noncommercial" to "yes" (e.g. via
  the Isabelle/jEdit menu Plugin Options / Isabelle / General)

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

Re: [isabelle-dev] Isabelle build timing on high-end hardware

[Lawrence Paulson]

These speedups are certainly very impressive! I have wondered what sort of 
factor could be achieved with enough cores, but was never persistent enough in 
trying to borrow hardware from people who had it.

Larry

> On 2 Jul 2018, at 14:21, Makarius  wrote:
> 
> Just for the fun of it, here are some timings on truly high-end
> hardware: some colleagues have upgraded recently and granted me access
> to make some tests.
> 
> The results may help others in their hardware decisions.
> 
> Here is an Executive Summary:
> 
>  * Intel Xeon performs better than AMD
>  * fewer NUMA nodes are better
>  * SSD file-systems help to save and load heap images fast
> 
> 
> Here are some details:
> 
> 2 * Intel(R) Xeon(R) Gold 6148 CPU @ 2.40GHz;
> 2 NUMA nodes: distance factor 2.1 for memory access;
> each CPU with 20 cores and hyper-threading: total of 80 hardware threads
> 
> 256 GB SSD
> 
> Ubuntu Linux 16.04
> 
> 
> Isabelle/eb53f944c8cd + AFP/f7e9efc65d82
> ISABELLE_BUILD_OPTIONS="threads=6"
> 
> 
> * 64bit: ML_OPTIONS="--minheap 3g --maxheap 30g"
> 
> Finished HOL (0:02:21 elapsed time, 0:07:13 cpu time, factor 3.07)
> 
> isabelle build -j10 -a -N -f
> 0:13:37 elapsed time, 5:12:16 cpu time, factor 22.91
> 0:18:02 elapsed time, 5:57:58 cpu time, factor 19.85
> 
> isabelle build -j10 -a -N -f -x HOL-Proofs
> 0:15:24 elapsed time, 5:11:24 cpu time, factor 20.20
> 0:14:12 elapsed time, 4:45:27 cpu time, factor 20.10
> 
> isabelle build -j10 -g main -N -f
> 0:07:56 elapsed time, 0:43:58 cpu time, factor 5.53
> 0:08:07 elapsed time, 0:44:33 cpu time, factor 5.48
> 
> 
> * 32bit: ML_OPTIONS="--minheap 1500"
> 
> Finished HOL (0:02:10 elapsed time, 0:06:42 cpu time, factor 3.10)
> 
> isabelle build -j10 -a -N -f
> 0:11:13 elapsed time, 3:24:13 cpu time, factor 18.20
> 0:12:05 elapsed time, 4:07:12 cpu time, factor 20.45
> 
> isabelle build -j10 -a -N -f -x HOL-Proofs
> 0:09:13 elapsed time, 3:37:16 cpu time, factor 23.55
> 0:09:02 elapsed time, 3:27:56 cpu time, factor 22.99
> 
> isabelle build -j10 -g main -N -f
> 0:07:02 elapsed time, 0:39:45 cpu time, factor 5.64
> 0:07:02 elapsed time, 0:39:28 cpu time, factor 5.61
> 
> 
> isabelle build -j4 -o threads=10 -g main -N -f
> 0:06:17 elapsed time, 0:46:10 cpu time, factor 7.34
> 0:05:58 elapsed time, 0:45:26 cpu time, factor 7.60
> 
> isabelle build -j6 -o threads=8 -g main -N -f
> 0:06:40 elapsed time, 0:43:18 cpu time, factor 6.49
> 
> 
> When trying out changes of Pure or HOL, I usually test "-g main" first:
> it consists of HOL, HOL-Algebra, HOL-Analysis,
> HOL-Computational_Algebra, HOL-Library, HOL-Number_Theory,
> HOL-Probability, HOL-SPARK, HOL-Word, HOLCF. Afterwards there is a high
> chance that all of Isabelle works.
> 
> The numbers above are really good for that: 6min and 12min respectively.
> These are "quasi-interactive" builds as they should be today.
> 
> 
>   Makarius
> ___
> 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

[isabelle-dev] Is hgbroy down?

[Lawrence Paulson]

~/isabelle/Repos/src/HOL: hg fetch
remote: ssh: connect to host hgbroy.informatik.tu-muenchen.de port 22: 
Operation timed out
abort: no suitable response from remote hg!

Larry

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

Re: [isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

[Lawrence Paulson]

Okay, I have replaced it by Complex_Main. In fact derivatives are only needed 
in a couple of places.
Larry

> On 28 Jun 2018, at 17:03, Florian Haftmann 
>  wrote:
> 
>> Is it right for this theory to base itself on HOL.Deriv rather than 
>> Complex_Main?
>> 
>> Larry
>> 
>> section ‹Polynomials as type over a ring structure›
>> 
>> theory Polynomial
>> imports
>>  HOL.Deriv
>>  "HOL-Library.More_List"
>>  "HOL-Library.Infinite_Set"
>>  Factorial_Ring
>> begin
> 
> I don't think so, especially the combination of theories from
> HOL-Library with a non-canonical theory entry is weird.
> 
> I am unable to tell on the spot how this has emerged.  Are there any
> suspicious things when HOL.Deriv is replaces by Complex_Main?
> 
> I guess that theory uses some analytical results and hence cannot build
> on Main alone.



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] HOL/Computational_Algebra/Polynomial.thy

[Lawrence Paulson]

Is it right for this theory to base itself on HOL.Deriv rather than 
Complex_Main?

Larry

section ‹Polynomials as type over a ring structure›

theory Polynomial
imports
  HOL.Deriv
  "HOL-Library.More_List"
  "HOL-Library.Infinite_Set"
  Factorial_Ring
begin

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

Re: [isabelle-dev] Isabelle build only works in certain directories

[Lawrence Paulson]

My last email was premature, because the exact same thing happened again: it 
hung at 2:15 minutes of CPU time. Fortunately I was able to kill it and retry, 
and thanks to multithreading, you don't have to wait anything like two minutes 
before reaching the two minute mark.

Larry

> On 28 Jun 2018, at 14:58, Lawrence Paulson  wrote:
> 
> I wonder whether this relates to the problem I have seen from time to time, 
> where the build process "goes to sleep" around two minutes into building HOL. 
> It's reproducible enough that I can feel confident that HOL will build only 
> when the activity monitor shows that the process has consumed at least three 
> minutes of CPU time. But I haven't seen it for a couple of weeks. 
> 
> I am (currently) running macOS High Sierra 10.13.5 but there may have been an 
> OS update during that time. It may be worth updating your system and trying 
> again.
> 
> Larry
> 
>> On 28 Jun 2018, at 12:25, Max Haslbeck  wrote:
>> 
>> 
>> I have the following curious problem: isabelle build only seems to work when 
>> I’m in certain directories.
>> 
>> Steps to reproduce:
>> 1. Start out with clean mercurial repository of isabelle in 
>> '/Users/mhaslbeck/Projects/isabelle'
>> 2. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -I'
>> 3. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -a'
>> 4. run 'cd /'
>> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>> Output:
>> ```
>> ### Building Isabelle/Scala ...
>> Started at Thu Jun 28 13:03:18 GMT+2 2018 (polyml-5.7.1_x86-darwin on 
>> lap44-cl-c703)
>> ISABELLE_BUILD_OPTIONS=""
>> 
>> ML_PLATFORM="x86-darwin"
>> ML_HOME="/Users/mhaslbeck/.isabelle/contrib/polyml-5.7.1-6/x86-darwin"
>> ML_SYSTEM="polyml-5.7.1"
>> ML_OPTIONS="--minheap 500"
>> 
>> Session Pure/Pure
>> ```
>> 6. The build process now freezes and doesn’t react to keyboard input, can be 
>> killed by 'pkill java'
>> 7. run 'mkdir ~/tmp; cd ~/tmp'
>> 8. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>> freezes with same output as in 5.
> 

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

Re: [isabelle-dev] Isabelle build only works in certain directories

[Lawrence Paulson]

I wonder whether this relates to the problem I have seen from time to time, 
where the build process "goes to sleep" around two minutes into building HOL. 
It's reproducible enough that I can feel confident that HOL will build only 
when the activity monitor shows that the process has consumed at least three 
minutes of CPU time. But I haven't seen it for a couple of weeks. 

I am (currently) running macOS High Sierra 10.13.5 but there may have been an 
OS update during that time. It may be worth updating your system and trying 
again.

Larry

> On 28 Jun 2018, at 12:25, Max Haslbeck  wrote:
> 
> 
> I have the following curious problem: isabelle build only seems to work when 
> I’m in certain directories.
> 
> Steps to reproduce:
> 1. Start out with clean mercurial repository of isabelle in 
> '/Users/mhaslbeck/Projects/isabelle'
> 2. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -I'
> 3. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle components -a'
> 4. run 'cd /'
> 5. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>  Output:
> ```
> ### Building Isabelle/Scala ...
> Started at Thu Jun 28 13:03:18 GMT+2 2018 (polyml-5.7.1_x86-darwin on 
> lap44-cl-c703)
> ISABELLE_BUILD_OPTIONS=""
> 
> ML_PLATFORM="x86-darwin"
> ML_HOME="/Users/mhaslbeck/.isabelle/contrib/polyml-5.7.1-6/x86-darwin"
> ML_SYSTEM="polyml-5.7.1"
> ML_OPTIONS="--minheap 500"
> 
> Session Pure/Pure
> ```
> 6. The build process now freezes and doesn’t react to keyboard input, can be 
> killed by 'pkill java'
> 7. run 'mkdir ~/tmp; cd ~/tmp'
> 8. run '/Users/mhaslbeck/Projects/isabelle/bin/isabelle build -v Pure'
>  freezes with same output as in 5.

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

[isabelle-dev] Bad session structure

[Lawrence Paulson]

I still get this upon start-up. Any idea why?

ebdd5508f386+ tip

Larry

Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Priority_Queue_Braun.Priority_Queue_Braun") (line 7 of 
"/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/Priority_Queue_Braun.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Priority_Queue_Braun" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Priority_Queue_Braun/ROOT")
Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Amortized_Complexity.Skew_Heap_Analysis" via 
"Skew_Heap.Skew_Heap") (line 7 of 
"/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Amortized_Complexity" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Amortized_Complexity/ROOT")
Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Skew_Heap.Skew_Heap") (line 7 of 
"/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/Skew_Heap.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Skew_Heap" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Skew_Heap/ROOT")
Cannot load theory "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred for theory "HOL-Data_Structures.Priority_Queue"
(required by "Pairing_Heap.Pairing_Heap_Tree") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/Pairing_Heap_Tree.thy")
No such file: "HOL-Data_Structures.Priority_Queue"
The error(s) above occurred in session "Pairing_Heap" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Pairing_Heap/ROOT")
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] quaternions

[Lawrence Paulson]

The cross product development is 200 lines long while the quaternion 
development is 730. Should they be separate entries, or do cross products 
belong elsewhere?
Larry

> On 18 Jun 2018, at 13:18, Tobias Nipkow  wrote:
> 
> Why not simply the AFP?



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] quaternions

[Lawrence Paulson]

I have just formalised most of the HOL Light development of quaternions. It's a 
great advertisement for type classes: showing that quaternions constitute a 
real normed division algebra and an inner product space supersedes most of the 
HOL Light proofs (many files), which are devoted to developing the arithmetic 
and topological properties of quaternions. In the course of this, I also ported 
the HOL Light development of the three-dimensional vector cross product.

So where does this material belong? Arguably not in Analysis, which is already 
too large.

Another question: I did not port the quaternion material relating to the 
constant reflect_along, which is defined as follows:

(* Reflection of a vector about 0 along a line. *)

let reflect_along = new_definition
 `reflect_along v (x:real^N) = x - (&2 * (x dot v) / (v dot v)) % v`;;

Is this concept useful, and if so, where does it belong?

Larry

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

I just tried

isabelle jedit -R HOL-UNITY

assuming that it would build an auxiliary image for HOL-Auth, which is 
imported. It built HOL-Auth rather than HOL-UNITY_requirements(HOL-Auth) so 
things are pretty subtle here. A little more explanation would be valuable.

Larry

> On 6 Jun 2018, at 16:36, Makarius  wrote:
> 
> It could just mean that these examples don't need an auxiliary image.
> 
> Take the first example from NEWS:
> 
>  isabelle jedit -R HOL-Number_Theory
> 
> It produces an image
> "HOL-Number_Theory_requirements(HOL-Computational_Algebra)", see also
> the title line of Isabelle/jEdit.
> 
> It also puts you into the ROOT entry for HOL-Number_Theory, so you can
> directly explore its theories in the Prover IDE.

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

> On 6 Jun 2018, at 12:43, Makarius  wrote:
> 
> On 06/06/18 12:45, Lawrence Paulson wrote:
>> I saw them of course, but what do they do?
> 
> These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
> have simplified and clarified the situation, updated NEWS and
> documentation in the "jedit" manual.
> 
> Right now the main question is if this is sufficient for the release,
> and the documentation clear.

Having tinkered with these things, read the NEWS entry and read the relevant 
section of the manual, I am still completely in the dark.

According to the NEWS entry, option -R builds an auxiliary logic image. I tried 
this with a couple of examples and no images were built. According to the 
manual, this option opens the ROOT entry. It does seem to do that, though I'm 
not sure why this facility is needed.

Surely it wouldn't be difficult to add a few lines of text, describing the sort 
of situation in which this option is useful.

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

I saw them of course, but what do they do?
Larry

> On 5 Jun 2018, at 22:19, Makarius  wrote:
> 
> On 05/06/18 23:06, Lawrence Paulson wrote:
>> I’d find an example helpful, as your brief description is pretty cryptic.
>> Larry
>> 
>>> On 5 Jun 2018, at 22:01, Makarius  wrote:
>>> 
>>> These options are very relevant for the coming release. I am interested
>>> to get feedback from early adopters, if this is already sufficient or
>>> requires further refinement.
> 
> The NEWS contains these examples:
> 
>  Examples:
>isabelle jedit -R HOL-Number_Theory
>isabelle jedit -R HOL-Number_Theory -A HOL
>isabelle jedit -d '$AFP' -S Formal_SSA -A HOL
>isabelle jedit -d '$AFP' -S Formal_SSA -A HOL-Analysis
> 
> Here are more examples:
> 
>isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Analysis
>isabelle jedit -d '$AFP' -S Deep_Learning -A HOL-Probability
>isabelle jedit -d '$AFP' -S Deep_Learning
> 
> Alexander Bentkamp needs to be credited for writing a clear
> specification of the intermediate image Deep_Learning_Lib: {* Theories
> that are not part of HOL-Probability but are used by this entry *}.
> 
> From there it was reasonably easy to implement the above options, but
> users need to start using them, and stop publishing old development
> artefacts in AFP.
> 
> 
>   Makarius

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

Re: [isabelle-dev] NEWS: isabelle jedit options

[Lawrence Paulson]

I’d find an example helpful, as your brief description is pretty cryptic.
Larry

> On 5 Jun 2018, at 22:01, Makarius  wrote:
> 
> These options are very relevant for the coming release. I am interested
> to get feedback from early adopters, if this is already sufficient or
> requires further refinement.

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

Re: [isabelle-dev] Cannot build HOL (again)

[Lawrence Paulson]

Then I get 

Unknown JAVA_HOME -- Java unavailable


Larry

> On 21 May 2018, at 18:17, Florian Haftmann 
>  wrote:
> 
> Do the problems persist if you remove ~/.isabelle e.g. to ~/.isabelle_tmp?

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

Re: [isabelle-dev] Cannot build HOL (again)

[Lawrence Paulson]

Well, it worked on the third attempt. Same as two weeks ago. My guess is that 
it pauses to wait for some resource: when it stalls, the process is still 
visible but only uses 0.1% of the processor.

Larry

> On 21 May 2018, at 15:13, Manuel Eberl  wrote:
> 
> It works fine for me.
> 
> Did you perhaps switch on ML debugging/exception tracing? HOL becomes
> virtually impossible to build with that switched on. What is the content
> of your ".isabelle/etc/preferences”?

(* generated by Isabelle 25-Apr-2018 17:11:02 +0100 *)

auto_methods = "true"
auto_nitpick = "true"
auto_time_limit = "7.0"
auto_time_start = ".5"
auto_try0 = "false"  (* unknown *)
editor_output_state = "true"
editor_prune_delay = "60.0"
editor_skip_proofs = "false"  (* unknown *)
jedit_macos_application = "true"  (* unknown *)
jedit_macos_preferences = "false"  (* unknown *)
jedit_print_mode = "brackets"
jedit_tooltip_delay = "0.5"
parallel_proofs_threshold = "100"  (* unknown *)
sledgehammer_provers = "e spass vampire z3 cvc4 "
sledgehammer_timeout = "60"
z3_non_commercial = "yes"  (* unknown *)

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

[isabelle-dev] Cannot build HOL (again)

[Lawrence Paulson]

I am continuing to be plagued by HOL failing to build, stalling quite 
reproducibly after about two minutes of processor time. It's a big obstacle to 
getting any work done, so tips would be welcome.

Larry

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

Re: [isabelle-dev] Failure and slowdown of JinjaThreads (due to merge desaster?)

[Lawrence Paulson]

> On 15 May 2018, at 14:51, Makarius  wrote:
> 
> Maybe also a campaign to get rid of unnecessary syntax ambiguity.

Totally. Most of the time it is completely unnecessary 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] HOL-Algebra

[Lawrence Paulson]

I’m talking about HOL-Algebra, and as I’ve seen myself, parts of it are 
ancient. They desperately need updating and streamlining.

We’ve decided that Group-Ring-Module is irremediable, and are using it only as 
a list of useful results that need to be done again.

Larry

> On 11 May 2018, at 23:40, Makarius  wrote:
> 
> Is the chaotic naming in Group-Ring-Module or HOL-Algebra? According to
> my information, Clemens Ballarin has taken great care about HOL-Algebra
> over many years (even with contributions by students).
> 

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

Re: [isabelle-dev] bad session structure

[Lawrence Paulson]

It seems that I can fix this by updating afp-devel again.
Larry

> On 9 May 2018, at 12:37, Lars Hupel  wrote:
> 
> Do you have any uncommitted changes? Maybe in the AFP?
> 
> ~/work/isabelle (default)$ isabelle-dev build -bva -D '$AFP'
> 
> works fine for me.

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

[isabelle-dev] bad session structure

[Lawrence Paulson]

I'm getting this message again. What gives? Everything is fully updated.

~/isabelle/Repos/src/HOL: hg id
2e5b737810a6 tip

Larry

Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category3.Limit" via "Category3.FreeCategory" via 
"Category3.Category") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/Category3/Category.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Category3" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Category3/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category2.MonadicEquationalTheory" via "Category2.Category") 
(line 8 of "/Users/lp15/isabelle/afp/devel/thys/Category2/Category.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Category2" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Category2/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Topology.LList_Topology" via "Topology.Topology") (line 10 of 
"/Users/lp15/isabelle/afp/devel/thys/Topology/Topology.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Topology" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Topology/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Category.Cat") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/Category/Cat.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Category" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Category/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Card_Partitions.Card_Partitions" via 
"Card_Partitions.Set_Partition") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Card_Partitions/Set_Partition.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Bell_Numbers_Spivey" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Bell_Numbers_Spivey/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Graph_Theory.Graph_Theory" via "Graph_Theory.Subdivision" via 
"Graph_Theory.Funpow") (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Graph_Theory/Funpow.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Graph_Theory" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Graph_Theory/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "Card_Partitions.Card_Partitions" via 
"Card_Partitions.Set_Partition") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Card_Partitions/Set_Partition.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Card_Partitions" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Card_Partitions/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "VectorSpace.FunctionLemmas") (line 6 of 
"/Users/lp15/isabelle/afp/devel/thys/VectorSpace/FunctionLemmas.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "Deep_Learning_Lib" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Deep_Learning/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "ArrowImpossibilityGS.GS" via "ArrowImpossibilityGS.Arrow_Order") 
(line 5 of 
"/Users/lp15/isabelle/afp/devel/thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "ArrowImpossibilityGS" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/ArrowImpossibilityGS/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "VectorSpace.VectorSpace" via "VectorSpace.MonoidSums" via 
"VectorSpace.FunctionLemmas") (line 6 of 
"/Users/lp15/isabelle/afp/devel/thys/VectorSpace/FunctionLemmas.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "VectorSpace" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/VectorSpace/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "LinearQuantifierElim.QEdlo" via "LinearQuantifierElim.DLO" via 
"LinearQuantifierElim.QE" via "LinearQuantifierElim.Logic") (line 6 of 
"/Users/lp15/isabelle/afp/devel/thys/LinearQuantifierElim/Thys/Logic.thy")
No such file: "HOL-Library.FuncSet"
The error(s) above occurred in session "LinearQuantifierElim" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/LinearQuantifierElim/ROOT")
Cannot load theory "HOL-Library.FuncSet"
The error(s) above occurred for theory "HOL-Library.FuncSet"
(required by "VectorSpace.VectorSpace" via "VectorSpace.MonoidSums" via 

[isabelle-dev] HOL-Algebra

[Lawrence Paulson]

I have two interns from École Polytechnique. They have been going over 
HOL-Algebra and Group-Ring-Module, providing new proofs of the best results in 
the latter and tidying up some messy proofs in the former, as well. They are 
also systematising the chaotic naming conventions that they found there. So 
there will be big changes to HOL-Algebra in the coming weeks. This is an early 
warning in case anybody else wants to work on this directory.

Larry

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

Re: [isabelle-dev] HOL build process hangs

[Lawrence Paulson]

Larry

> On 3 May 2018, at 13:48, Makarius <makar...@sketis.net> wrote:
> 
> On 03/05/18 14:04, Lawrence Paulson wrote:
>>> 
>>> What is your changeset id?
>> 
>> ~/isabelle/Repos/src/HOL: hg id
>> 8dc792d440b9+ tip
> 
> That is after my change 0acf3206a723. Did you see the problem in
> 36209dfb981e, too?

I have no idea how I could answer this question, as these change numbers appear 
to be absolutely random. I have recently been pulling changes every morning and 
I saw similar symptoms yesterday.

> What are the build options, e.g. the bottom of the output of "isabelle
>>> build -?” ?
> 
> The "isabelle build" tool with argument "-?" emits various settings for
> convenience. 

  ISABELLE_BUILD_OPTIONS=""
  
  ML_PLATFORM="x86-darwin"
  ML_HOME="/Users/lp15/.isabelle/contrib/polyml-5.7.1-5/x86-darwin"
  ML_SYSTEM="polyml-5.7.1"
  ML_OPTIONS="-H 1000"


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

Re: [isabelle-dev] HOL build process hangs

[Lawrence Paulson]

> On 3 May 2018, at 12:56, Makarius <makar...@sketis.net> wrote:
> 
> On 03/05/18 13:18, Lawrence Paulson wrote:
>> I'm encountering a strange phenomenon: the HOL build process runs for just 
>> over two minutes (which is not long enough to complete) and then seems to 
>> stop running, using 0.1% of the processor. I can repeat it and the same 
>> thing happens again. Today I was lucky on the third attempt. What could 
>> cause the build to hang and do nothing?
> 
> What is your changeset id?

~/isabelle/Repos/src/HOL: hg id
8dc792d440b9+ tip

> What is the underlying hardware?

Mac Pro (2013), 3.5GHz 6-Core Xeon E5 with 16GB

> What are the build options, e.g. the bottom of the output of "isabelle
> build -?” ?

One was “isabelle jedit ” and the other was this:

~/isabelle/Repos/src/HOL: isabelle build -b HOL
Building HOL ...
^C^C^C*** Interrupt
HOL FAILED
Unfinished session(s): HOL
0:08:42 elapsed time, 0:02:13 cpu time, factor 0.25
^C^C


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

[isabelle-dev] HOL build process hangs

[Lawrence Paulson]

I'm encountering a strange phenomenon: the HOL build process runs for just over 
two minutes (which is not long enough to complete) and then seems to stop 
running, using 0.1% of the processor. I can repeat it and the same thing 
happens again. Today I was lucky on the third attempt. What could cause the 
build to hang and do nothing?

Larry

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

[isabelle-dev] Bad session structure: may cause problems with theory imports

[Lawrence Paulson]

In the past couple of days, upon launching Isabelle jEdit, I get an alert box 
with the message above and the attached text. Any ideas?

Larry

~/isabelle/Repos/src/Pure: hg id
362baebe25a5 tip

Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "Affine_Arithmetic.Affine_Arithmetic" via 
"Affine_Arithmetic.Ex_Affine_Approximation" via "Affine_Arithmetic.Print") 
(line 8 of "/Users/lp15/isabelle/afp/devel/thys/Affine_Arithmetic/Print.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "HOL-ODE-Refinement" (line 19 of 
"/Users/lp15/isabelle/afp/devel/thys/Ordinary_Differential_Equations/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "JinjaThreads.Basic_Main") (line 5 of 
"/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/Basic/Basic_Main.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "JinjaThreads" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/JinjaThreads/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via 
"CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via 
"CAVA_Base.Code_String") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "Maxflow_Lib" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Flow_Networks/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char" (line 14 of 
"/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "Iptables_Semantics" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Iptables_Semantics/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "FOL_Harrison.FOL_Harrison") (line 14 of 
"/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/FOL_Harrison.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "FOL_Harrison" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/FOL_Harrison/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "LTL.LTL_Example") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/LTL/example/LTL_Example.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "LTL" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/LTL/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "LLL_Factorization.Modern_Computer_Algebra_Problem") (line 13 of 
"/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/Modern_Computer_Algebra_Problem.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "LLL_Factorization" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/LLL_Factorization/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "Native_Word.Native_Cast") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Native_Word/Native_Cast.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "Native_Word" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Native_Word/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via 
"CAVA_Base.Code_String") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "CAVA_Base" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "Transition_Systems_and_Automata.NBA_Explicit" via 
"Transition_Systems_and_Automata.NBA_Nodes" via "DFS_Framework.Reachable_Nodes" 
via "DFS_Framework.DFS_Framework" via "DFS_Framework.Param_DFS" via 
"CAVA_Base.CAVA_Base" via "CAVA_Base.CAVA_Code_Target" via 
"CAVA_Base.Code_String") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/CAVA_Automata/CAVA_Base/Code_String.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in session "Transition_Systems_and_Automata" (line 
3 of "/Users/lp15/isabelle/afp/devel/thys/Transition_Systems_and_Automata/ROOT")
Cannot load theory "HOL-Library.Code_Char"
The error(s) above occurred for theory "HOL-Library.Code_Char"
(required by "Knuth_Morris_Pratt.KMP") (line 4 of 
"/Users/lp15/isabelle/afp/devel/thys/Knuth_Morris_Pratt/KMP.thy")
No such file: "HOL-Library.Code_Char"
The error(s) above occurred in 

Re: [isabelle-dev] Complete Distributive Lattice

[Lawrence Paulson]

I don’t think it’s a problem that your more general theorems require the Axiom 
of Choice, and Hilbert_Choice.thy is not too large already (far from it).

Larry Paulson



> On 8 Mar 2018, at 21:35,  
>  wrote:
> 
> I have a question about how to organize these changes. The problem is that 
> most of the results for the more general lattice (instantiations 
> to set, fun) require Hilbert_Choice which is not available in 
> Complete_Lattice. Now I have added all results about complete distributive 
> lattices that need Hilbert Choice in Hilbert_Choice.thy. Is this acceptable?
> 

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

Re: [isabelle-dev] [isabelle] Matrix-Vector operation

[Lawrence Paulson]

Is there a realistic prospect for uniting these two formalisations of linear 
algebra?
Larry

> On 27 Feb 2018, at 11:05, Thiemann, Rene  wrote:
> 
> But indeed, Fabian is completely right that lemmas for determinants, etc. are 
> duplicates. Actually, the JNF-matrices “‘a mat” 
> have been developed from scratch (without HMA_Connect), by manually copying 
> and adapting several proofs from the distribution.

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

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Lawrence Paulson]

I was at the meeting in Logroño and my impression was that we had to live with 
these different formalisations. There was no way to unify them and the best one 
could hope to transfer certain results from one formalisation to another using 
local types in some incredibly complicated way.

If there really is a common basis for formalising linear algebra than I would 
be thrilled to see it, and I'm sure we could figure out a way to implement this.

Larry

> On 26 Feb 2018, at 14:57, Fabian Immler  wrote:
> 
> We do have the problem that AFP/Jordan_Normal_Form/Matrix and 
> Analysis/Finite_Cartesian_Product both formalize vectors and matrices and 
> that there are formalizations of (aspects of) linear algebra for both of 
> them. Last year in Logrono, there was the proposal to put all linear algebra 
> on the common foundation of a locale for modules, but apparently nobody has 
> found the time and motivation to push this much further.
> 
> Perhaps a more humble first step towards unifying the existing theories would 
> be to move AFP/Jordan_Normal_Form/Matrix to the distribution and do the 
> construction of Finite_Cartesian_Product.vec as a subtype of Matrix.vec.
> 
> Any opinions on that?



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

[Lawrence Paulson]

Is there a case for moving some material from this file into the Analysis 
directory?

https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
 


Many of the results proved at the end of this file are quite straightforward 
anyway. As somebody with a lifting-and-transfer phobia, I don't feel qualified 
to make this decision. Possibly these techniques are overkill. I have already 
proved some of these results quite straightforwardly using linearity, and 
installed them not long ago.

Larry

> Begin forwarded message:
> 
> From: Fabian Immler 
> Subject: Re: [isabelle] Matrix-Vector operation
> Date: 26 February 2018 at 08:02:40 GMT
> To: isabelle-users 
> Cc: Omar Jasim 
> 
> Dear Omar,
> 
> Unfortunately, there are no lemmas on distributivity of *v in the 
> distribution.
> Some are currently in the AFP-entry Perron_Frobenius:
> https://www.isa-afp.org/browser_info/current/AFP/Perron_Frobenius/HMA_Connect.html
> 
> You can prove them (in HOL-Analysis) as follows:
> 
> lemma matrix_diff_vect_distrib: "(A - B) *v v = A *v v - B *v (v :: 'a :: 
> ring_1 ^ 'n)"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum_subtractf left_diff_distrib)
> 
> lemma matrix_add_vect_distrib: "(A + B) *v v = A *v v + B *v v"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum.distrib distrib_right)
> 
> lemma matrix_vector_right_distrib: "M *v (v + w) = M *v v + M *v w"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum.distrib distrib_left)
> 
> lemma matrix_vector_right_distrib_diff: "(M :: 'a :: ring_1 ^ 'nr ^ 'nc) *v 
> (v - w) = M *v v - M *v w"
>  unfolding matrix_vector_mult_def
>  by vector (simp add: sum_subtractf right_diff_distrib)
> 
> Those should probably be included in the next Isabelle release.
> 
> Hope this helps,
> Fabian
> 
> 
>> Am 25.02.2018 um 19:27 schrieb Omar Jasim :
>> 
>> Hi,
>> 
>> This may be trivial but I have a difficulty proving the following lemma:
>> 
>> lemma
>> fixes  A :: "real^3^3"
>>   and x::"real^3"
>> assumes "A>0"
>> shows " (A *v x) - (mat 1 *v x)  = (A - mat 1) *v x "
>> 
>> where A is a positive definite diagonal matrix. Is there a lemma predefined
>> related to this?
>> 
>> Cheers
>> Omar
> 



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] NEWS: formal comments

[Lawrence Paulson]

Will there still be a way to comment out random junk? I often work with a 
mixture of Isabelle and commented-out HOL Light material.

Larry

> On 26 Jan 2018, at 20:19, Makarius  wrote:
> 
> * Old-style inner comments (* ... *) within the term language are legacy
> and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›"
> instead.

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

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

[Lawrence Paulson]

I'd prefer to keep things simple. I do like your recent syntactic innovations, 
but such things need to be introduced with care. And the inner syntax is 
considerably more delicate.
Larry

> On 2 Feb 2018, at 10:50, Makarius  wrote:
> 
> The general concept behind it is implicit abstraction, here with
> explicit (( ... )) to delimit its scope (different notation would be
> required in reality):
> 
>  ((a + _))  ~> %x. a + x
>  ((_ + a))  ~> %x. x + a
>  ((a + _ + b + _))  ~>  %x y. a + x + b + y
>  ((_ < a))  ~> %x. x < a
> 
> E.g.
> 
>  filter ((_ < a)) list
>  map ((_ - a)) list
>  All ((_ < a))
>  Collect ((_ < a))
> 
> We already have implicit underscore treatment for clausal definitions,
> so the above would not be totally alien. (But I am not proposing to do
> anything concrete now.)

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

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

[Lawrence Paulson]

Happy to agree
Larry

> On 1 Feb 2018, at 16:23, Tobias Nipkow  wrote:
> 
> I think (simple) sections do indeed improve readbility. BUT in the light of 
> your comments I am not keen on them in Isabelle.


signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Gromov Hyperbolicity

[Lawrence Paulson]

I'm afraid I've no idea. I didn't study much analysis for my first degree, not 
even the basics of complex analysis.

Larry

> On 18 Jan 2018, at 14:29, Tobias Nipkow  wrote:
> 
> So what is the situation wrt the theories I asked about?

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

Re: [isabelle-dev] Gromov Hyperbolicity

[Lawrence Paulson]

This is mainly a negative criterion, i.e., something outside the undergraduate 
curriculum probably should not be in our core libraries. But I would guess for 
example mathematicians cover Gödel's theorem, which we would not want to move 
to our core libraries.

Larry

> On 18 Jan 2018, at 13:31, Tobias Nipkow  wrote:
> 
> It sounds like a reasonable criterion. Can you tell us what that means for 
> Hausdorff_Distance, Metric_Completion and Isometries (as detailed by Fabian)?

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

Re: [isabelle-dev] Gromov Hyperbolicity

[Lawrence Paulson]

We certainly need to solve this problem. One possible criterion: which results 
are part of a standard undergraduate  athematics curriculum?
Larry

> On 18 Jan 2018, at 10:06, Fabian Immler  wrote:
> 
> We do not have a precise specification of what HOL-Analysis is or should be. 
> I think that makes it very hard to draw a line between material that should 
> go to HOL-Analysis and what should remain in the AFP. So take this as just my 
> personal view.



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] New AFP entry Gromov Hyperbolicity in devel

[Lawrence Paulson]

I wonder whether some of this material should be moved to the Analysis library.
Larry

> On 18 Jan 2018, at 06:51, Tobias Nipkow  wrote:
> 
> Along the way, we introduce basic material on isometries, quasi-isometries, 
> Lipschitz maps, geodesic spaces, the Hausdorff distance, the Cauchy 
> completion of a metric space, and the exponential on extended real numbers.



signature.asc
Description: Message signed with OpenPGP
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

[Lawrence Paulson]

I know how to do it, but no beginner could ever find this.
Larry

> On 16 Jan 2018, at 16:20, Andreas Lochbihler  
> wrote:
> 
> It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter 
> "brackets" under Print mode.

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

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

[Lawrence Paulson]

> On 16 Jan 2018, at 14:13, Blanchette, J.C.  wrote:
> 
> However, for operators like ==>, which bind on the right,
> 
>   foo ==>
>   bar
> 
> is actually much more readable than
> 
>   foo
>   ==> bar

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.

>   foo ==> bar
>   ==> baz

As for this last example, we definitely need the earlier syntax [|foo; bar|] 
==> baz, which has been made almost impossible to enable.

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

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

[Lawrence Paulson]

> On 10 Jan 2018, at 21:26, Makarius  wrote:
> 
> The Haskell community appears to have picked up a lot of such (slightly
> odd) styles from Lamport. E.g. they put commas at the start of the line
> instead of the end, which is typographically very strange.
> 
> I was educated by the original TeX Book, which in turn refers to the
> top-quality mathematical typesetting from around 1900. Here the
> operators and commas are in the traditional position: end of line.

I got in the habit of putting arithmetic operators at the start of a line while 
at university, having made too many errors from forgetting that the symbol at 
the end of the previous line was a minus sign. Of course, that consideration 
doesn't apply to commas, and it's amazing that Lamport (and Dijkstra?) managed 
to persuade people to adopt such crazy conventions.

Interactive theorem proving isn't the same thing as solving physics problems by 
hand, so I'm not against having operators at the end of the line if that's what 
people think would be best. Note however that the equals sign is an infix 
operator and is invariably put at the start of a line, never at the end.

Larry

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

Re: [isabelle-dev] font issues in Isabelle jedit

[Lawrence Paulson]

I seem to have fixed the problem by selecting

File > Reload with encoding > UTF-8-Isabelle

Larry

> On 2 Jan 2018, at 22:05, Lawrence Paulson <l...@cam.ac.uk> wrote:
> 
> But after letting the system build again, the result is the same as before.
> 

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

Re: [isabelle-dev] font issues in Isabelle jedit

[Lawrence Paulson]

> On 2 Jan 2018, at 19:21, Makarius  wrote:
> 
> I have changed the fonts again recently, see Isabelle/ecb74607063f. I've
> made a brief test on my MacMini with High Sierra, and it appears to work.
> 
> 
> Normally "isabelle components -a" should give you the resulting ttf
> files, and Isabelle/jEdit should pick them up.
> 
> This can be prevented by having IsabelleText.ttf / IsabelleTextBold.ttf
> installed on the system by accident (on macOS in some Library/Fonts
> directory, FontBook should be able to tell you). You should remove such
> spurious copies of the Isabelle fonts.

I didn’t have any copies in those places, but I deleted all the copies in the 
contib directory, did “hg fetch” and finally

~/isabelle/Repos/src/HOL: isabelle components -a
### Missing Isabelle component: 
"/Users/lp15/.isabelle/contrib/isabelle_fonts-20171230"
Getting "https://isabelle.in.tum.de/components/isabelle_fonts-20171230.tar.gz;
Unpacking "/Users/lp15/.isabelle/contrib/isabelle_fonts-20171230.tar.gz"
~/isabelle/Repos/src/HOL: hg id
17fdb2c98083 tip

But after letting the system build again, the result is the same as before.

Larry

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

[isabelle-dev] font issues in Isabelle jedit

[Lawrence Paulson]

Fonts have been weird for me for some time (clearly wider than jedit “thinks” 
they are) but now symbols are completely missing. E.g. I see

  have "integral UNIV (indicator (S \ T)) = integral UNIV (\a. 
if a \ S \ T then 1::real else 0)"

Any idea what could be wrong? I’m using

> 6afba546f0e5 tip

Larry

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

Re: [isabelle-dev] Haskabelle unmaintained

[Lawrence Paulson]

Deleted from Cambridge.
Larry

> On 9 Dec 2017, at 12:16, Makarius  wrote:
> 
> Since the mirror rsync procedure is conservative by default, the other
> mirror sites should also remove haskabelle.html manually.

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

Re: [isabelle-dev] weird error message on startup

[Lawrence Paulson]

I was able to fix the problem by going to the afp-devel directory and typing 
“hg fetch". I guess some big incompatible changes had taken place.
Larry

> On 6 Dec 2017, at 22:32, Makarius <makar...@sketis.net> wrote:
> 
> On 06/12/17 15:48, Lawrence Paulson wrote:
>> I've just updated to a recent version (fa1173288322) and tried to run a 
>> session by the following command:
>> 
>> isabelle jedit -l HOL-Analysis CV.thy 
>> 
>> And then I get an alert box containing the appended text. Any idea what's 
>> going wrong here?
> 
> It looks like you have an alien AFP version in your ROOTS or -d options,
> one that does not fit to the Isabelle version.

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

[isabelle-dev] weird error message on startup

[Lawrence Paulson]

I've just updated to a recent version (fa1173288322) and tried to run a session 
by the following command:

isabelle jedit -l HOL-Analysis CV.thy 

And then I get an alert box containing the appended text. Any idea what's going 
wrong here?

Larry

Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
The error(s) above occurred for theory "Markov_Models.Probability"
(required by "Markov_Models.Markov_Models" via 
"Markov_Models.Markov_Models_Auxiliary") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Markov_Models_Auxiliary.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/Probability.thy"
The error(s) above occurred in session "Markov_Models" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Markov_Models/ROOT")
[ line 12 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_App.thy"] 
error: keyword "begin" expected,
but string was found:
"\t"


^
The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_App"
(required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy")
[ line 15 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Std.thy"] 
error: keyword "begin" expected,
but string was found:
"\t"


^
The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_KBO_Std"
(required by "Lambda_Free_KBOs.Lambda_Free_KBOs" via 
"Lambda_Free_KBOs.Lambda_Free_KBO_Basic") (line 9 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBO_Basic.thy")
[ line 16 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy"]
 error: keyword "begin" expected,
but string was found:
">p"


^
The error(s) above occurred for theory "Lambda_Free_KBOs.Lambda_Free_TKBO_Coefs"
(required by "Lambda_Free_KBOs.Lambda_Free_KBOs") (line 12 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/Lambda_Free_KBOs.thy")
The error(s) above occurred in session "Lambda_Free_KBOs" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Lambda_Free_KBOs/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
The error(s) above occurred for theory "MFMC_Countable.Probability"
(required by "Probabilistic_While.While_SPMF" via 
"MFMC_Countable.Rel_PMF_Characterisation" via 
"MFMC_Countable.Matrix_For_Marginals" via "MFMC_Countable.MFMC_Misc") (line 6 
of "/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/MFMC_Misc.thy")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy"
The error(s) above occurred for theory "Probabilistic_While.Probability"
(required by "Probabilistic_While.Bernoulli") (line 8 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Bernoulli.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/MFMC_Countable/Probability.thy"
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/Probability.thy"
The error(s) above occurred in session "Probabilistic_While" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_While/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
The error(s) above occurred for theory "Probabilistic_System_Zoo.Probability"
(required by "Probabilistic_System_Zoo.Probabilistic_Hierarchy") (line 5 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probabilistic_Hierarchy.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/Probability.thy"
The error(s) above occurred in session "Probabilistic_System_Zoo" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Probabilistic_System_Zoo/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy"
The error(s) above occurred for theory "Randomised_Social_Choice.Probability"
(required by "Randomised_Social_Choice.Randomised_Social_Choice" via 
"Randomised_Social_Choice.SDS_Lowering" via 
"Randomised_Social_Choice.Social_Decision_Schemes") (line 13 of 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Social_Decision_Schemes.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/Probability.thy"
The error(s) above occurred in session "Randomised_Social_Choice" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Randomised_Social_Choice/ROOT")
Cannot load theory file 
"/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy"
The error(s) above occurred for theory "Quick_Sort_Cost.Probability"
(required by "Quick_Sort_Cost.Randomised_Quick_Sort") (line 10 of 
"/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy")
No such file: 
"/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/Probability.thy"
The error(s) above occurred in session "Quick_Sort_Cost" (line 3 of 
"/Users/lp15/isabelle/afp/devel/thys/Quick_Sort_Cost/ROOT")
Cannot load theory file 

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Lawrence Paulson]

Whatever happened with this? The new release has been out for a while, and it 
would make sense to integrate your work now, well before any thought of a new 
release.
Larry

> On 27 Aug 2017, at 15:59, Viorel Preoteasa <viorel.preote...@aalto.fi> wrote:
> 
> I managed to integrate the new complete distributive lattice into HOL library.
> 
> The changes are these:
> 
> Complete_Lattice.thy
> - replaced the complete_distrib_lattice with the new stronger version.
> - moved some proofs about complete_distrib_lattice and some instantiations to 
> Hilbert_Choice
> 
> Hilbert_Choice.thy
> - added all results complete_distrib_lattice, including instantiations
> of set, fun that uses uses Hilbert choice.
> 
> Enum.thy
> - new proofs that finite_3 and finite_4 are complete_distrib_lattice.
> - I added here the classes finite_lattice and finite_distrib_lattice
> and proved that they are complete. This simplified quite much the proofs
> that finite_3 and finite_4 are complete_distrib_lattice.
> 
> Predicate.thy
> - new proof that predicates are complete_distrib_lattice.
> 
> I compiled HOL in Isabelle2017-RC0 using
> 
> isabelle build -v -c HOL
> 
> and I got:
> 
> Timing HOL (2 threads, 266.231s elapsed time, 487.094s cpu time, 43.344s GC 
> time, factor 1.83)
> Finished HOL (0:04:26 elapsed time)
> 
> Finished at Sun Aug 27 17:41:30 GMT+3 2017
> 0:04:37 elapsed time
> 
> But I don't now how to go from here to have these changes into Isabelle.
> 
> There is also AFP. If there are instantiations of complete_distrib_lattice, 
> then most probably they will fail.
> 
> One simple solution in this case could be to keep also the
> old complete_distrib_lattice as complete_pseudo_distrib_lattice.
> 
> Viorel
> 
> 
> On 8/26/2017 3:06 PM, Lawrence Paulson wrote:
>>> On 25 Aug 2017, at 20:14, Viorel Preoteasa <viorel.preote...@aalto.fi 
>>> <mailto:viorel.preote...@aalto.fi>> wrote:
>>> 
>>> One possible solution:
>>> 
>>> Add the new class in Complete_Lattice.thy, replacing the existing class
>>> 
>>> Prove the instantiations and the complete_linearord subclass later
>>> in Hilbert_Choice.
>>> 
>>> On the other hand, it seems inconvenient to have the Hilbert Choice
>>> to depend on so many other theories.
>> I’d prefer this provided the instantiations aren’t needed earlier.
>> The delay in the introduction of the Axiom of Choice is partly historical, 
>> but it’s worth noting how much of HOL can be developed without it.
>> Larry

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

Re: [isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

This makes sense. Many thanks!
Larry

> On 3 Nov 2017, at 13:13, Makarius  wrote:
> 
> * Only the most fundamental theory names are global, usually the entry
> points to major logic sessions: Pure, Main, Complex_Main, HOLCF, IFOL,
> FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for
> formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK".
> 

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

Re: [isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

It’s nice that global theories don’t have to be qualified. But it’s a bit 
strange that it's forbidden to qualify them.

--lcp

> On 2 Nov 2017, at 17:21, Makarius <makar...@sketis.net> wrote:
> 
>> On 02/11/17 17:47, Lawrence Paulson wrote:
>> 
>> And I have triple checked that Probability is spelt correctly. Any hints?
> 
> Since Isabelle/f27488f47a47 you can use completion there (on the theory
> base name).
> 
> E.g. "ALi" completes "HOL-Library.AList".
> 
> 
>Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] the new "imports" semantics

[Lawrence Paulson]

I’ve been converting some theories from the old pathname syntax to the new 
setup. I have the line

imports "HOL-Probability.Probability”

but it is rejected with the message

Bad theory import "HOL-Probability.Probability"

If instead I import "HOL-Probability.Random_Permutations” or 
"HOL-Probability.Central_Limit_Theorem” it works fine. And I have triple 
checked that Probability is spelt correctly. Any hints?

Larry

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

Re: [isabelle-dev] Future of Nat_Transfer

[Lawrence Paulson]

I have never understood it and generally feel terror at the sight of any 
transfer operation. So I would be happy to get rid of it.
Larry

> On 19 Oct 2017, at 12:56, Florian Haftmann 
>  wrote:
> 
> My suggestion would be to remove it completely.
> 
> Any opinions on that?

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

[isabelle-dev] NEWS

[Lawrence Paulson]

Session HOL-Analysis: Moebius functions and the Riemann mapping theorem.

Larry

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

Re: [isabelle-dev] AFP statistics

[Lawrence Paulson]

We can be very proud of these figures. I have occasionally compared the source 
releases of Certain Other Systems over time, and noticed that proofs are still 
write-only: new proofs are added, but existing proofs are almost never changed.

Larry

> On 28 Sep 2017, at 13:20, Tobias Nipkow  wrote:
> 
> The whole project started with this AFP paper:
> 
> http://www21.in.tum.de/~nipkow/pubs/cicm15.html 
> 
> 
> First Max developed this just to support the statistics in the paper but then 
> he and Lars made it part of the AFP. There is also a hidden part that 
> generates tex files for these and a number of further statistics that I use 
> for talks.
> 
> Concerning growth of articles. I am not sure we want to provide more 
> finegrained statistics for every entry, but attached you find a summary 
> slide. I cannot remember precisely what is measured, but at a first 
> approximation it tells us that over time every second line of an AFP entry is 
> modified.
> 
> Tobias

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

Re: [isabelle-dev] Complete Distributive Lattice

[Lawrence Paulson]

For sure. The work is very welcome, but too drastic to undertake at this 
precise moment.
Larry

> On 28 Aug 2017, at 13:08, Makarius  wrote:
> 
> Nothing of this is relevant for the Isabelle2017 release. When the "RC"
> versions show up, it is time to finish and not to start new things.

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

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Lawrence Paulson]

In the AFP, grep picks up these:

~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .
./Coinductive/Examples/CCPO_Topology.thy
./Concurrent_Ref_Alg/Refinement_Lattice.thy
./DataRefinementIBP/Diagram.thy
./DataRefinementIBP/Hoare.thy
./DataRefinementIBP/Statements.thy
./LatticeProperties/Conj_Disj.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran.thy
./MonoBoolTranAlgebra/Mono_Bool_Tran_Algebra.thy
./PSemigroupsConvolution/Quantales.thy

But why would they fail? The new version is surely stronger, so any changes 
should be pretty straightforward, right? 

Larry

> On 27 Aug 2017, at 15:59, Viorel Preoteasa  wrote:
> 
> There is also AFP. If there are instantiations of complete_distrib_lattice, 
> then most probably they will fail.
> 
> One simple solution in this case could be to keep also the
> old complete_distrib_lattice as complete_pseudo_distrib_lattice.
> 

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

Re: [isabelle-dev] Towards the Isabelle2017 release - Complete Distributive Lattice

[Lawrence Paulson]

> On 25 Aug 2017, at 20:14, Viorel Preoteasa  wrote:
> 
> One possible solution:
> 
> Add the new class in Complete_Lattice.thy, replacing the existing class
> 
> Prove the instantiations and the complete_linearord subclass later
> in Hilbert_Choice.
> 
> On the other hand, it seems inconvenient to have the Hilbert Choice
> to depend on so many other theories.

I’d prefer this provided the instantiations aren’t needed earlier.

The delay in the introduction of the Axiom of Choice is partly historical, but 
it’s worth noting how much of HOL can be developed without it. 

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

Re: [isabelle-dev] Towards the Isabelle2017 release

[Lawrence Paulson]

Sounds good to me. Can anybody think of an objection?
Larry

> On 23 Aug 2017, at 15:17, Viorel Preoteasa  wrote:
> 
> Hello,
> 
> I am not sure if this is the right place to post this message, but it is
> related to  the upcoming release as I am prosing adding something
> to the Isabelle library.
> 
> While working with complete distributive lattices, I noticed that
> the Isabelle class complete_distrib_lattice is weaker compared to
> what it seems to be regarded as a complete distributive lattice.
> 
> As I needed the more general concept, I have developed it,
> and if Isabelle community finds it useful to be in the library,
> then I could provide the proofs or integrate it myself in the
> Complete_Lattice.thy
> 
> The only axiom needed for complete distributive lattices is:
> 
> Inf_Sup_le: "Inf (Sup ` A) ≤ Sup (Inf ` {f ` A | f . (∀ Y ∈ A . f Y ∈ Y)})"
> 
> and from this, the equality and its dual can be proved, as well as
> the existing axioms of complete_distrib_lattice and the instantiation
> to bool, set and fun.
> 
> Best regards,
> 
> Viorel
> 
> 
> On 2017-08-21 21:24, Makarius wrote:
>> Dear Isabelle contributors,
>> 
>> we are now definitely heading towards the Isabelle2017 release.
>> 
>> The first official release candidate Isabelle2017-RC1 is anticipated for
>> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
>> 
>> That is also the deadline for any significant additions.
>> 
>> 
>> I have already updated the important files NEWS, CONTRIBUTORS, ANNOUNCE
>> in Isabelle/5c0a3f63057d, but it seems that many potential entries are
>> still missing.
>> 
>> Please provide entries in NEWS and CONTRIBUTORS for all relevant things
>> you have done since the last release.
>> 
>> 
>>  Makarius
>> ___
>> 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

___
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

[Lawrence Paulson]

I’ve been using it a bit and it’s pretty useful! Thanks
Larry

> On 9 Jul 2017, at 17:16, Fabian Immler  wrote:
> 
> A while ago, Florian Haftmann sent a command that does something like this to 
> the mailing list [1]. I attach a version that works with current 
> Isabelle2016-1 (not sure if I got all the modifications right, but it seems 
> to work at least on the example in the .thy file).

___
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

[Lawrence Paulson]

No, that’s precisely what I’d like to avoid. I prefer texts that you can 
actually read. It would be great to have something automatically generated, 
even if it needed manual tweaking (e.g. to rename variables).

And I’ve gone to some effort purging instances of “guess” from existing proofs.

Larry

> On 8 Jul 2017, at 22:16, Peter Lammich  wrote:
> 
> We already have proof goal_cases. Is that what you mean?

___
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

[Lawrence Paulson]

I am always using the new auto-complete facility for 

proof (cases “...”) 

and for induction. But could this be done for “proof" with any method, simply 
copying out the states of the subgoals? Then people would make a lot less use 
of “subgoals”, etc.

Larry

> On 5 Jul 2017, at 21:04, Makarius  wrote:
> 
> Is there anything else to take into account for this late-summer release
> process?

___
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

[Lawrence Paulson]

What’s the idea here?
Larry

> On 5 Jul 2017, at 21:09, Manuel Eberl  wrote:
> 
> the proper printing of "nat" values as numerals instead of successor notation.

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

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Lawrence Paulson]

As I recall, this constant originally comes from HOL Light and is used in a 
couple of proofs.

And it occurs to me that it might be a good way of dealing with HOL Light’s 
generalisation of summations and limits to sets of natural numbers. As I ported 
the PNT, I used two other methods of dealing with that problem.

At the moment I don’t regard it as heavily used, but I guess it depends on what 
one is working on at any one time.

I would rather have qualified names than completely arbitrary variations of the 
name.

Larry

> On 30 Jun 2017, at 15:57, Manuel Eberl  wrote:
> 
> Still, I for one think this is not really worth the trouble of keeping an 
> entirely separate constant around, especially because "subseq h" does not 
> make much sense: "h" itself is not a subsequence of anything, "f ∘ h" is a 
> sub-sequence of "f".
> 
> It would be interesting to know what other users of Complex_Main think about 
> that.
> 
> 

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

Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates

[Lawrence Paulson]

Indeed we do.
Larry

> On 28 Jun 2017, at 18:49, Manuel Eberl  wrote:
> 
> Yes, I noticed that as well. I decided to leave it that way since, well,
> we do have qualified names.

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

Re: [isabelle-dev] Poly/ML 5.7

[Lawrence Paulson]

Version 5.7 doesn’t even build on my main workstation, though it works on my 
MacBook Pro running broadly similar software. No idea what is going on here, 
but I’m not happy about it.
Larry

> On 15 May 2017, at 11:14, Makarius  wrote:
> 
> David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago
> (see https://github.com/polyml/polyml/releases/tag/v5.7), but announced
> it only last week.
> 
> I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that
> is only for testing, not for production use. Some results can be seen here:
> 
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
> http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html
> 
> The test hardware is similar or actually the same as "Linux A", but this
> needs to be investigated further. It is also important to compare
> timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task
> is still busy digging into older history.
> 
> 
> After the substantial changes of the code generator and representation
> of ML values in memory, there are various open questions concerning
> performance and robustness of Isabelle applications.
> 
> This means, we need to skip the Poly/ML 5.7 release and stay on the last
> Poly/ML 5.6 until the situation becomes more clear.
> 
> 
> This is how to use the polyml-5.7 component locally:
> 
>  $ edit $ISABELLE_HOME_USER/etc/settings
> 
>  init_component "$HOME/.isabelle/contrib/polyml-5.7"
> 
>  $ isabelle components -a
> 
> 
>   Makarius
> ___
> 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] Isabelle build status with timing information

[Lawrence Paulson]

Thanks for those graphs, which are really interesting. Note in particular the 
sharp drops in elapsed time or heap for Analysis, Probability, Algebra and 
several others. What gets the credit for this?

Larry

> On 10 May 2017, at 10:55, Makarius  wrote:
> 
> After a delay of some weeks (actually several months since October 2016)
> there is now an updated version of the classic Isabelle build status
> with timing information, see
> http://isabelle.in.tum.de/devel/build_status and its source
> http://isabelle.in.tum.de/repos/isabelle/annotate/96b4799a2e04/src/Pure/Admin/isabelle_devel.scala#l82
> 
> 
> This demonstrates that it is still possible to produce performance
> charts in the quality that we've known from the past. Two main factors
> are relevant for this:
> 
>  (1) The physical measurements need to be done without disturbance by
> other processes, especially no other test processes running in parallel
> on the same CPU/memory node. (The numactl tool can be a great help.)
> 
>  (2) Data plotting requires care about the gnuplot installation. For
> reasons that I don't understand, various Linux distributions (e.g
> Gentoo) can show quite bad interpolation in gnuplot, and make the data
> look worse than it really is. For the above, I have just compiled
> gnuplot-5.0.6 from the original source and suddenly it worked smoothly.
> 
> 
> The data for the charts is collected as plain log files for archival
> purposes in /home/isatest/cronjob/log/ at TUM. This directory is
> uploaded every day to a PostgreSQL database server in the background
> (only accessible by "isatest"). It can then be used with tools like
> "isabelle build_status" to make the charts.
> 
> In addition, there is a small database snapshot in SQLite format:
> http://isabelle.in.tum.de/devel/build_log.db -- e.g. for exploration
> with sqlitebrowser (which also supports minimal plotting). Here is an
> example query for its "Execute SQL" window:
> 
> SELECT pull_date, heap_size FROM isabelle_build_log
> WHERE session_name = 'HOL-Analysis' AND  build_host = 'lxbroy9' AND
> threads = 1
> ORDER BY pull_date
> 
> Comparing this with threads = 2 shows that heap images produced by a
> multi-threaded build process are slightly bigger, which I did not know
> before. So this is one of the usual starting points for performance and
> resource usage tuning, based on such relevant performance measurements.
> 
> 
> There is more in the data that is not plotted yet, e.g. the precise
> relation of tests run with threads=1,2,4,6. Or online heap usage, thread
> activity, future tasks, etc. for an individual process (ml_statistics).
> 
> At last we are no longer "flying blind" ...
> 
> 
>   Makarius
> ___
> 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] [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main

[Lawrence Paulson]

As I understand it, the star notation is the standard way of denoting the 
injection of an entity from, say, the standard reals to the non-standard reals. 
It is normally written as a prefix operator. Maybe we could do something using 
our  ⋆ character. But we have two other naming conventions in NSA: the prefixes 
hr and NS. 

A lot of work needs to be done in order to bring this development up-to-date. 
I’m glad to see that the star operator is now fully integrated into the 
axiomatic type class system, but quite a lot of material made redundant by that 
step is still present.

Larry

> On 3 Mar 2017, at 09:28, Makarius <makar...@sketis.net> wrote:
> 
> On 27/02/17 18:22, Lawrence Paulson wrote:
>> 
>> Note: I have no suggestions for improving the star notation of
>> non-standard analysis, mentioned in the last paragraph.
> 
> Can you point to some literature or papers that use the notation in a
> canonical form?
> 
> 
>   Makarius
> 
> 

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