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 warning,
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
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 regressions
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:
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 sy
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
lifting/trans
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
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: Makar
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 adding unsigned 64 bit integers to the AFP entry Native_Wor
We already have proof goal_cases. Is that what you mean?Peter Original Message Subject: Re: [isabelle-dev] The coming release of Isabelle2017From: Lawrence Paulson To: Markus Wenzel CC: isabelle-dev I am always using the new auto-complete facility for proof (cases “...”) and for in
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:
> > >
> > >
On So, 2016-12-04 at 22:30 +0100, Makarius wrote:
> On 04/12/16 11:14, Lars Hupel wrote:
> >
> > >
> > > Where did you see these lots of Unsynchronized.ref (or better
> > > Synchronized.var) in Isabelle Tools?
> > There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools",
> > 181
> > in
This was an artificial counterexample, which I tried out of curiosity, but having applications like caching of already proved theorems in mind.Peter Originalnachricht Betreff: Re: [isabelle-dev] Circular reasoning via multithreading seems too easyVon: Makarius An: Peter Lammich
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 trac
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 ???
>
--
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
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 p
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 have
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 cla
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 v
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, depe
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
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 tes
* 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 it
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
>
> 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 c
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 abo
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 root.l
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 editin
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
date:
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
O
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 no
>
> 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 abo
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
p
Hi.
Is there any reason why the obvious split-lemmas for Option.bind are not
included in Option.thy?
lemma bind_split: "P (bind m f)
⟷ (m = None ⟶ P None) ∧ (∀v. m=Some v ⟶ P (f v))"
by (cases m) auto
lemma bind_split_asm: "P (bind m f) = (¬(
m=None ∧ ¬P None
∨ (∃x. m=Some
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)+
lemm
> However, the constructions might still be useful, as the following comment
> from Peter
> Lammich's AFP entry Refine_Monadic shows.
>
>(* TODO: Library/Quickcheck_Types.thy:flat_complete_lattice provides
> an isomorphic contruction. *)
At this point I duplicated the flat complete lat
Hi,
I recently ran into a method that produced a stack-overflow.
The good thing is: In the current jedit version, it is properly
highlighted and you immediately see that there is some error. (This was
not always the case in the past)
The bad thing: The only way how to get a clue what is going wr
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
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 experimenta
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
> 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 sh
> 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
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
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
http://afp.
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 power
So, ad-hoc massaging of a lemma is no longer possible?
E.g., I often use things like
by (auto ... dest!: sym[of "pop A", standard] ...)
in cases where I definitely do not want to expose the subgoal where the
"pop = ..." occurs into Isar.
So, if I got it right, the correct way would now be:
> 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 c
--- Begin Message ---
Extended Submission Deadlines
Abstract submission: December 27, 2013
Contribution submission: December 30, 2013
[Please apologies for multiple copies.]
Call
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 ei
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
> 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 Exn.I
se 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:
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
>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, sch
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:
https://mailmanbroy.
Oops, that was me! Sorry, it was a test of mine, that I obviously forgot
to remove.
The whole export_code - block can be removed, I'll do it in afp-devel,
but someone has to remove it in the snapshot.
--
Peter
On Do, 2013-10-31 at 08:44 +0100, Florian Haftmann wrote:
> In thys/JinjaThreads/Ex
On Di, 2013-10-01 at 14:12 +0900, Christian Sternagel wrote:
> Thanks Jasmin!
>
> @Peter: Does this patch work with your developments as expected?
>
At first glance, everything looks fine! Thank you for fixing this.
--
Peter
p.s. I've commited the patch, it's e13b0c88c798
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 a
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
reason
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
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 f
> 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
https
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, e
Forwarding this error report to the right mailing list ...
--- Begin Message ---
Referring to Isabelle_12-Sep-2013:
When using overloading from Monad_Syntax, abbreviations are no longer
displayed in output syntax:
theory Scratch
imports
Main
"~~/src/HOL/Library/Monad_Syntax"
begin
abbrevi
> 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 Simplifie
Almost always I use <-->. The only exception being a comparison of
booleans, like in "if (a::bool) = b then ..."
-- Peter
On Di, 2013-09-03 at 09:33 +0900, Christian Sternagel wrote:
> Same here. - cheers chris
>
> Florian Haftmann wrote:
>
> >> Are there clubs of "iff" vs. "non-iff"? If alm
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
matc
On Do, 2013-02-14 at 17:22 +, Lawrence Paulson wrote:
> In a dream scenario, one might imagine opening a document containing a number
> of occurrences of "sorry", and each one of these occurrences would be given
> to counterexample finders and to sledgehammer, without any specific user
> int
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. Shou
On Di, 2012-11-20 at 14:47 +0100, Makarius wrote:
> On Wed, 17 Oct 2012, Makarius wrote:
>
> > Does anybody remember a use of the 'apply_end' command? Many years ago
> > it was introduced to help analyse the failure of 'qed', in symmetry to
> > 'apply' to break up 'proof' and 'by' steps. That s
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
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 JEdi
The same may happen with constants, and I was already confused several
times, when the interpretation command failed due to this effect. Using
locale expressions and forgetting to add name prefixes (a!:, b!:, etc)
can easily cause this effect.
So I also vote for an error message (or at least a war
> 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 sh
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 sep
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 be
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
> >>> restri
On Mo, 2012-04-02 at 13:45 +0200, Makarius wrote:
> On Mon, 26 Mar 2012, Peter Lammich wrote:
>
> > I tried to follow the approach done in the cancellation simprocs,
> > getting something like:
> >
> > fun assn_simproc_fun ss credex = let
> >val ctxt =
> 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 t
> 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
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
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
... 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
https://mailmanbroy.informatik.tu-muenchen.de/
>> 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
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 littl
86 matches
Mail list logo
