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

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:

Re: [isabelle-dev] Current AFP problems

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

[isabelle-dev] Redundant definitions in Analysis

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

Re: [isabelle-dev] infix line breaking

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

Re: [isabelle-dev] infix line breaking

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

Re: [isabelle-dev] infix line breaking

c 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 &g

[isabelle-dev] infix line breaking

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

Re: [isabelle-dev] Analysis not building

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 >

Re: [isabelle-dev] Analysis not building

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

[isabelle-dev] Analysis not building

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?

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

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

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

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

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

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

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

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

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

Re: [isabelle-dev] mercurial accident

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

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

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

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

> 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

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

> 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

[isabelle-dev] illegal reflective access

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:

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

> 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

Re: [isabelle-dev] Lemma "sum_image_le"

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 >

Re: [isabelle-dev] Frag / Poly_Mapping

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

Re: [isabelle-dev] Frag / Poly_Mapping

> 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

[isabelle-dev] Frag / Poly_Mapping

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 /

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

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

Re: [isabelle-dev] performance problems

> 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

Re: [isabelle-dev] performance problems

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

[isabelle-dev] performance problems

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

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

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

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

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

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

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

Re: [isabelle-dev] Vampire

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

Re: [isabelle-dev] Vampire

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

[isabelle-dev] Vampire

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

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

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

[isabelle-dev] Is hgbroy down?

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

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

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

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

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

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

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

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

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

[isabelle-dev] Bad session structure

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

Re: [isabelle-dev] quaternions

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

[isabelle-dev] quaternions

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

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

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

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

> 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

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

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

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

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

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

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

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

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

[isabelle-dev] Cannot build HOL (again)

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

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

> 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

Re: [isabelle-dev] HOL-Algebra

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

Re: [isabelle-dev] bad session structure

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] bad session structure

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

[isabelle-dev] HOL-Algebra

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

Re: [isabelle-dev] HOL build process hangs

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

Re: [isabelle-dev] HOL build process hangs

> 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

[isabelle-dev] HOL build process hangs

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

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

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

Re: [isabelle-dev] Complete Distributive Lattice

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

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

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

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

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

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

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

Re: [isabelle-dev] NEWS: formal comments

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

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

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

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

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

Re: [isabelle-dev] Gromov Hyperbolicity

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?

Re: [isabelle-dev] Gromov Hyperbolicity

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,

Re: [isabelle-dev] Gromov Hyperbolicity

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.

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

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,

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

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.

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

> 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

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

> 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

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

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

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

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

[isabelle-dev] font issues in Isabelle jedit

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

Re: [isabelle-dev] Haskabelle unmaintained

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

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

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

[isabelle-dev] weird error message on startup

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

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

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_distr

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

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

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

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 t

[isabelle-dev] the new "imports" semantics

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”

Re: [isabelle-dev] Future of Nat_Transfer

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

[isabelle-dev] NEWS

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

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

Re: [isabelle-dev] Complete Distributive Lattice

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

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

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

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

> 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

Re: [isabelle-dev] Towards the Isabelle2017 release

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

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

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

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

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.

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

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,

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

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

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

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

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

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

Re: [isabelle-dev] Poly/ML 5.7

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

Re: [isabelle-dev] Isabelle build status with timing information

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

Re: [isabelle-dev] [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main

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

  1   2   3   4   5   >