Re: [isabelle-dev] syntax highlighting of inner comments

Hi FabianI already pointed out the missing highlighting of cancel a few months ago ... I am still strongly in favor of having a highlighting that can easily be distinguished, eg the legacy red, or perhaps gray ...Right now, when using Isabelle 2018, I do not use cancel, but (**), getting a

Re: [isabelle-dev] Isabelle DejaVu against old Isabelle Text font

No luck on my machine. The font rendering still looks slightly blurred.  However, I'm using an old Linux (Ubuntu 16.04) ... may that be the reason? --   Peter On So, 2019-02-10 at 20:01 +0100, Christian Sternagel wrote: > This is just to confirm that the result looks really great on my > linux

Re: [isabelle-dev] NEWS: generated code as proper theory export

Can you give some more details on how to achieve this? > > Concrete application: I have a verified SAT solver (lets call that 1. Gratchk is a similar use-case, where I need to export code, link it with some external ML code using MLton b/c it's faster, and test the result for timing

Re: [isabelle-dev] NEWS: generated code as proper theory export

On Do, 2019-01-31 at 16:03 +0100, Makarius wrote: > I have looked around at typical uses of 'export_code' in AFP. Most of > the time it is just informative: writing a file and looking at it in > the > editor (or via the command-line!?), or doing that on the output > channel. > The isabelle-export:

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

I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ... from my side there are no uses of this quotation remaining that I'd know ofHowever, (* *) is still very important for informally andquickly commenting things out, also in inner

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

I observed that "(=)" is hard to type in the default symbols setup, it will be folded to "\)" if immediate completion is on (A short informal poll in our group resulted that most of us have immediate completion on). When trying to write parametricity lemmas in predicate-style (eg for

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

On Di, 2018-01-16 at 16:31 +, Lawrence Paulson wrote: > I know how to do it, but no beginner could ever find this. > Larry This is usually one of the first things I show students learning Isabelle ... I'm using brackets syntax in demos, but let  them decide which syntax they like better. Peter

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

However, sort_by takes a function mapping the elements into a linear order, which is less general than allowing arbitrary (preorder?) relations.Peter Original Message Subject: Re: [isabelle-dev] [Spam] Fwd: added sorted_wrt to List; added Data_Structures/Binomial_Heap.thyFrom:

Re: [isabelle-dev] PolyML update

If there is really such a serious bug, we should update asap, imhoPeter Original Message Subject: [isabelle-dev] PolyML updateFrom: Andreas Lochbihler To: DEV Isabelle Mailinglist CC: Dear list,I've been playing around with

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

lse   by (tactic ‹resolve_tac @{context} [thm] 1›) (*ML ‹   Thm.join_proofs [thm]; ›*) end On So, 2016-12-04 at 23:13 +0100, Makarius wrote: > On 04/12/16 22:52, Peter Lammich wrote: > > > > On So, 2016-12-04 at 22:30 +0100, Makarius wrote: > > > > > >

Re: [isabelle-dev] Circular reasoning via multithreading seems too easy

net>An: Peter Lammich <lamm...@in.tum.de>,isabelle-dev <isabelle-...@in.tum.de>Cc: On 03/12/16 14:57, Peter Lammich wrote:> > the attached theory is accepted by all Isabelle's from 2015 to the> latest 2016-1-RC4, without any complaints, even in batch mode > (i

[isabelle-dev] Circular reasoning via multithreading seems too easy

Hi all, the attached theory is accepted by all Isabelle's from 2015 to the latest 2016-1-RC4, without any complaints, even in batch mode  (isabelle build).  It just uses a prove_future, and proves the theorem with itself! So, I have two questions here: 1. I always thought that there is some

Re: [isabelle-dev] Does Isabelle support code generation in C/C++ or maybe even java ???

Hi David, currently, the closest you can get is Scala, which can be linked to Java applications. Scala is supported out of the box by the code generator. --   Peter On Do, 2016-12-01 at 10:14 +, David Blubaugh wrote: > Does Isabelle support code generation in C/C++ or maybe even java ??? >

Re: [isabelle-dev] not-exists problem

Peter > > Michael > > On 13/09/2016, 18:41, "isabelle-dev on behalf of Tjark Weber" le-dev-boun...@mailbroy.informatik.tu-muenchen.de on behalf of tjark. > we...@it.uu.se> wrote: > > On Tue, 2016-09-13 at 09:45 +0200, Peter Lammich wrote: > > I would

[isabelle-dev] Code Folding and errors

Feature Request: (Isabelle: caae34eabcef) If an error appears in folded code, make it somehow visible in the main text window.  Currently, there is no indication of such an error that allows precise localization. Trying to jump to the error via clicking on the red bars on the left requires very

Re: [isabelle-dev] not-exists problem

On Di, 2016-09-13 at 00:46 +0100, Lawrence Paulson wrote: > We have a problem with the ∄ operator, when existential quantifiers > are nested: > > lemma "(∄x. ∃y. P x y) = (~(∃x y. P x y))" >   by (rule refl) I do not see a particular problem with this, however, not-exists and also exists-one

Re: [isabelle-dev] Multiset insert

On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote: > Tobias wrote: > > > How about > > > > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where > > "add# x M = {#x#} + M" This, however, may produce confusion with multiset union, which is an instance of the plus type

Re: [isabelle-dev] NEWS: type-inference for object-logic

Nice one, so we're not going to see the annoying "... not of sort 'type'" error any more, which used to occur occasionally in Isabelle/HOL developments!? -- Peter On Di, 2016-04-12 at 16:46 +0200, Makarius wrote: > *** General *** > > * Type-inference improves sorts of newly introduced type

Re: [isabelle-dev] lifting syntax with proper symbols

On Fr, 2016-03-04 at 14:13 +0100, Ondřej Kunčar wrote: > As Andreas already mentioned, we've been consistently using the symbol > \Mapsto for ===> in our papers. Concerning --->, we used \mapsto. In context of the Refinement Framework, I also use infix syntax for rel_prod (\\<^sub>r), which,

Re: [isabelle-dev] minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

Currently heating my CPU with test-building the patch ... If everything goes fine, I will push it. -- Peter On Do, 2015-11-19 at 10:46 +0100, Florian Haftmann wrote: > Hi all, > > >> These suggestions are worth a discussion. Should we go ahead? Would > anybody like to apply this patch and

Re: [isabelle-dev] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

On Mi, 2015-11-18 at 15:26 +, Lawrence Paulson wrote: > These suggestions are worth a discussion. Should we go ahead? Would anybody > like to apply this patch and test that everything still works? Pushed. See Isabelle-dev, changeset 2e89bc578935 -- Peter > > Larry > > > Begin forwarded

[isabelle-dev] NEWS: HOL/Library/Omega_Words_Fun

* HOL/Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a. This lived hidden in $AFP/Automatic_Refinement before, but other entries started to use it. So I moved it to HOL/Library. (Expecting $AFP/LTL_to_DRA to break until Salomon, who wants to adapt it himself, has fixed

[isabelle-dev] Cannot execute Poly/ML in 32bit mode

Hi list, When I start Isabelle, I get the following warning message on the console: ### Cannot execute Poly/ML in 32bit mode (missing shared libraries for C/C++) ### Using bulky 64bit version of Poly/ML instead Is it a problem to use the bulky 64bit version? -- Peter

Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context

On Do, 2015-04-02 at 00:16 +0200, Makarius wrote: * The main operations to certify logical entities are Thm.ctyp_of and Thm.cterm_of with a local context; Does this mean that you added functionality concerning the local context to the Isabelle kernel, which formerly did not know anything

Re: [isabelle-dev] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context

No, there is no fundamental change. Certification is a matter of the background theory of the context (the expansion of abbreviations is merely a historical accident). The change mainly avoids awkward use of Proof_Context.theory_of in regular Isabelle/ML sources -- it used to cause

[isabelle-dev] Someone messed up HOL_library/Multiset_Order

Isabelle version: devel -- hg id 034b13f4efae Test ended on: macbroy2, Thu Mar 26 13:46:35 CET 2015. HOL-Library FAILED (see also /home/isatest/afp/isabelle-afp-poly/heaps/polyml-5.5.2_x86-darwin/log/HOL-Library) Output written on root.pdf (710 pages, 1552625 bytes). Transcript written on

Re: [isabelle-dev] Reprocessing in Isabelle/jEdit

I noticed the same behaviour yesterday, with fe5b796d6b2a. This is very inconvenient, in particular if you have long-lasting proof methods or big goal outputs, this produces lots of additional load. -- Peter On Di, 2015-03-24 at 13:29 +0100, Jasmin Blanchette wrote: Hi all, When editing

Re: [isabelle-dev] Problem in the AFP

On Sa, 2015-03-21 at 18:26 +0100, Peter Lammich wrote: It's the operation identification phase of Autoref, quite difficult to debug ... I have not yet looked at it due to ITP-deadline. I found the culprit: changeset: 5269:88dc498667ff user:Rene Thiemann rene.thiem...@uibk.ac.at

Re: [isabelle-dev] Problem in the AFP

It's the operation identification phase of Autoref, quite difficult to debug ... I have not yet looked at it due to ITP-deadline. I will have look at it next week on Monday or Tuesday. Does anyone know the changeset that introduced the failure, or is there an easy way to find out? -- Peter

Re: [isabelle-dev] HOL/Number_Theory/Primes

Is this another application for the new NOMATCH simproc? -- Peter On Fr, 2014-11-07 at 18:34 +0100, Tobias Nipkow wrote: Thanks for finding this out. The theorem is a dvd b == b mod a = 0 This applies to any term a mod b and creates a subgoal a dvd b. Normally, that is not too bad.

[isabelle-dev] How to activate/de-activate unifier-trace from ML-level

Hi List, I have a tactic that has a debug-mode. In debug-mode, it shall output unification trace for certain (but not all) rule applications. How to write a tactic resolve_with_tracing: thm list - int - tactic that behaves like resolve_tac, but outputs unification trace? Best, Peter

Re: [isabelle-dev] How to activate/de-activate unifier-trace from ML-level

You can contribute indirectly to important reforms that are in the pipeline for a long time by keeping your sources in a more up-to-date state. As you said, there seems to be no other way of achieving what I required. I realized that, added a comment (*Argh!*) expressing my disgust about

Re: [isabelle-dev] rtrancl lemma proposal

Looks like a special case of simulation: lemma rtrancl_sim: assumes ⋀x y a. ⟦(x, y) ∈ r; (x,a)∈S⟧ ⟹ ∃b. (y,b)∈S ∧ (a, b) ∈ s and (x, y) ∈ r⇧* and (x,a)∈S shows ∃b. (y,b)∈S ∧ (a, b) ∈ s⇧* using assms(2, 1,3) by (induct) (fastforce intro: rtrancl.rtrancl_into_rtrancl)+ lemma

Re: [isabelle-dev] AFP: Failing entries

Finally, (after I have found out how to use afp_build) I could reproduce and fix the docuemnt preparation errors in the CAVA-entries, and now, according to afp-status, everything works fine. -- Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Remaining uses of Proof General?

That clickable area is convenient, but not strictly necessary. It is absent in PG anyway. Whenever the Prover IDE outputs an error message, e.g. in tooltips or the Output panel, it includes the source position information, *if* that is available. The problem is, that I cannot make the

Re: [isabelle-dev] Remaining uses of Proof General?

The default guess is that the JVM has too little heap space. You have called 4 GB unreasonably large before, which is an indication that your defaults are far too low. OK, I'll try more on my 8Gb machine ... or upgrade my machine. If problems happen again with 4-8 GB JVM heap, you

Re: [isabelle-dev] Remaining uses of Proof General?

On Fr, 2014-06-27 at 13:58 +0200, Makarius wrote: On Fri, 27 Jun 2014, Peter Lammich wrote: * Long list of warnings, e.g. duplicate simp rule, or tracing messages produced by a method appear before the subgoals in the output, and thus makes them inaccessible without lots of scrolling

Re: [isabelle-dev] Remaining uses of Proof General?

On Fr, 2014-06-27 at 14:22 +0200, Makarius wrote: On Fri, 27 Jun 2014, Peter Lammich wrote: If problems happen again with 4-8 GB JVM heap, you should describe what really happens, with clear experimental setup. Giving a clear experimental setup is a real problem for errors that appear

Re: [isabelle-dev] Remaining uses of Proof General?

Hi all. I have given Isabelle/jEdit another try and worked with it for almost two weeks, on different tasks: * Porting the CAVA afp entries (depending on 300 theory files) from 2013-2 to devel. * Formalizations and proof development (The standard usage) * Writing tools in ML (ML-blocks in

[isabelle-dev] AFP: Failing entries

Hi, yesterday, I have committed changes that should fix the CAVA-entries. Testboard has already seen my changes, and everything seems fine there: http://isabelle.in.tum.de/testboard/Isabelle/report/758870108e44469d8ea5688ab4610492 However, the revision 7774f1f22e30 mentioned on

Re: [isabelle-dev] Remaining uses of Proof General?

I'm still a regular user of PG. From time to time, I test Isabelle/jEdit, and my reasons for switching back to PG are somewhat similar to what Andreas reported. My main problems with Isabelle/JEdit are: 1. I cannot really control what Isabelle/Jedit processes when, and it invests computation

Re: [isabelle-dev] Safe approach to hypothesis substitution mark II

If there's interest in getting this change installed, I'll slog through these, and then figure out what's broken and what's expected to be broken in the latest tip of Isabelle and in the AFP. I'd call for volunteers to help with that bit though. I would very much appreciate such a

Re: [isabelle-dev] WG: [Semantics] Homework 6

Which version of Isabelle are you using, and which one have you used before, that was stable? -- Peter On Mo, 2013-12-02 at 23:29 +, Peter Maximilian Hirschbeck wrote: Die aktuelle Hausaufgabe ist im Anhang, oder zumindest das was davon übrig geblieben ist. Leider hat Isabelle bei

Re: [isabelle-dev] Isabelle2013-2 release

From your description, this looks like a timeout-problem to me ... while your machine is loaded by proving the theory, quickcheck times out. After the edit, there is less load, and quickcheck is faster. -- Peter On Do, 2013-11-21 at 10:40 +0100, Tobias Nipkow wrote: Am 20/11/2013 22:49,

Re: [isabelle-dev] Isabelle2013-2 release

On Do, 2013-11-21 at 12:21 +0100, Makarius wrote: On Wed, 20 Nov 2013, Lawrence Paulson wrote: Are there options that would reveal instances of this problem? It happens whenever you have something still running, but continue editing. The running tasks are errorneously interrupted and

Re: [isabelle-dev] Isabelle2013-2 release

by (tactic {* let val _ = stack_overflow 0 in all_tac end*}) ML_val {* Thm.peek_status @{thm f} *} -- Peter On Do, 2013-11-21 at 13:11 +0100, Makarius wrote: On Thu, 21 Nov 2013, Peter Lammich wrote: On my machine, there is also a second way to run into this Problem: Just load

Re: [isabelle-dev] Isabelle2013-2 release

If a breakdown happens as easily as editing the text, it is a problem. If it is merely a conceptual demonstration of breakability, if is not. Of course my example was synthetic. The question is: Are there currently real proof methods that may run out of stack space or otherwise throw

Re: [isabelle-dev] Isabelle2013-2 release

Addition: The stack-overflow problem already occurs in Isabelle2013, however, the theorem's status is unfinished here, but isabelle/jEdit also gives no indication of this. -- Peter On Do, 2013-11-21 at 14:56 +0100, Peter Lammich wrote: Finally, here is another way how isabelle-release

Re: [isabelle-dev] Concerning AFP 2a0f81020af9

On Do, 2013-10-31 at 10:57 +0100, Florian Haftmann wrote: The whole export_code - block can be removed, I'll do it in afp-devel, Thanks. but someone has to remove it in the snapshot. I meant the release branch of AFP, that Gerwin made a few days ago. See also:

[isabelle-dev] Testboard

Hi, I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard seems to have stopped processing it ... however, many later pushs have already run through completely. What's the strategy to get your push on testboard processed within

Re: [isabelle-dev] Testboard

it to the isabelle repository, how do I do it? Can I use Testboard? -- Peter On Fr, 2013-09-27 at 11:49 +0200, Lars Noschinski wrote: On 27.09.2013 09:16, Peter Lammich wrote: I pushed on testboard 19 hours ago, and my push (36cf426cb1c6) currently only shown as 1/3 processed. Now, testboard

Re: [isabelle-dev] Isabelle_25-Sep-2013 integration test

I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a bunch of error messages: tar: Ignoring unknown extended header keyword `SCHILY.ino' tar: Ignoring unknown extended header keyword `SCHILY.nlink' tar: Ignoring unknown extended header keyword `SCHILY.dev' ... And the unpacked

Re: [isabelle-dev] Isabelle_25-Sep-2013 integration test

Correction: The file unpacks correctly, the messages seem to be only warnings. I forgot to build the logic, immediately starting isabelle emacs. Peter On Do, 2013-09-26 at 10:01 +0200, Peter Lammich wrote: I cannot unpack the tar-file. My Linux (Ubuntu 12.04.2 LTS) gives me a bunch of error

Re: [isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable

Here a bisect would be helpful when this came to happen actually (or is it already present in Isabelle2013). This one already goes wrong in Isabelle2013. Cheers, Florian ___ isabelle-dev mailing list isabelle-...@in.tum.de

[isabelle-dev] Abbreviations + Monad_Syntax introduce unit itself additional type variable

Referring to Isabelle_2013 AND Isabelle_12_Sep_2013: In the following example, using an abbreviation that contains monad-syntax introduces a superfluous additional itself-parameter, that, however, is immediately instantiated to unit itself. Note that, when replacing abbreviation by definition,

Re: [isabelle-dev] Advice for replacing @{simpset} with @{context}.

The relevant text from NEWS is this: * Simplifier tactics and tools use proper Proof.context instead of historic type simpset. Old-style declarations like addsimps, addsimprocs etc. operate directly on Proof.context. Raw type simpset retains its use as snapshot of the main Simplifier

Re: [isabelle-dev] HOL-Codegenerator_Test fails in case-insensitive file-systems

Hi. We ran into this problem with Scala on Windows, our workaround was to either build a jar-file on linux, or do manual renaming in the Isabelle-sources. Isn't it possible to integrate case-insensitivity in the renaming that is performed by the code-generator anyway (to rename identifiers

[isabelle-dev] Resolve with premises

Hi all, as the question currently arose on the users list, I remembered that I have the following method laying around since several month. I'm using it frequently in apply-style scripts (Mainly to apply induction hypotheses). We discussed here in Munich whether we should add it to Isabelle.

Re: [isabelle-dev] NEWS: more informative errors in lazy enumerations

On Mi, 2012-10-17 at 11:09 +0200, Makarius wrote: *** ML *** * Type Seq.results and related operations support embedded error messages within lazy enumerations, and thus allow to provide informative errors in the absence of any usable results. Cool, no more writing of error messages to the

Re: [isabelle-dev] superfluous [?]

Hi It's always problematic if the user cannot be sure whether his theorem is actually proved, or the proof method is just diverging in a parallel thread. Thus, a UI should provide very clear information to the user, otherwise we will get Problem reports of the form: Everything runs fine in JEdit,

Re: [isabelle-dev] NEWS: Isabelle sessions and build management

In Collections and refine-monadic, as far as I can remember, there are two specialties: 1. We use a book document class rather than the default article, which required some fine-tuning of the documents. We use text_raw \chapter{...} instead of header . 2. We generate the userguide as a

Re: [isabelle-dev] NEWS: Isabelle sessions and build management

Is there really any *need* to have ruby produce theory sources? Browsing through the outcome briefly, it looks very conventional: a few document antiquotations and a few defininitions/theorems/interpretations issued in Isabelle/ML should do the job. The bit of Isabelle/ML should be

[isabelle-dev] Locale interpretation introduces abbreviations rather than definitions

Hi all, I have the problem that locale interpretation introduces abbreviations for locally defined constants, rather than definitions. This does not work well with the code generator. Is there a way to make locale interpretation introduce real definitions, and, if not, how much effort would it

Re: [isabelle-dev] Tweak Haskell output for future Haskell compatibility.

On Di, 2012-05-08 at 12:55 +0200, Tobias Nipkow wrote: Am 08/05/2012 12:41, schrieb Makarius: On Tue, 8 May 2012, Tobias Nipkow wrote: I mean the datatype definition facility. Over the years this lead to occasional confusion of end-users, who wanted to restrict their datatype

Re: [isabelle-dev] - and --

Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to

Re: [isabelle-dev] - and --

Anyway, who is maintaining Isabelle ProofGeneral now? The repository version does not work with Emacs 23 for several months already. It seems that nobody cares about it anymore. For the release, I will package up official ProofGeneral-4.1 as last time. It is then up to its users to

[isabelle-dev] Invoking Simplifier inside simproc, ### Simplifier: renamed bound variable

Hi all, Referring to Isabelle-2011-1 (If this post belongs to the users list, feel free to answer it there) I want to write a simplification procedure, that gets in a term t, does some transformations on it to obtain a term t', then invokes the simplifier (with some customized simpset) to prove

[isabelle-dev] I will start to fix my broken entries in afp-devel now

So if anyone else currently working on that, please tell me Best, Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] JinjaThreads in French!

... at least the superscripts of TOC and chapters, in the release-branch of AFP. Looks like it was built on a french latex configuration. Cheers, Peter ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] NEWS - Redundant lemmas

Perhaps we should start using a standardized process for phasing out legacy theorems, like moving them into a separate theory file Legacy.thy that would not be imported by default, and would be cleared out after each release. When upgrading Isabelle, users could import Legacy.thy as needed

Re: [isabelle-dev] [isabelle] Countable instantiation addition

This is definitely a useful tool for ImperativeHOL ... One could probably integrate it into the datatype package, such that datatypes automatically become countable (like Haskell infers some typeclasses automatically (on demand)) Peter Mathieu Giorgino schrieb: Hi all, I have written a