from:"Peter Lammich"

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

2011-07-21 Thread Peter Lammich

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 little ML library allowing to automatically prove, in most 
cases, instantiations of types (typedefs, records and datatypes) as countable 
(see ~~/src/HOL/Library/Countable). The style of the library is still a little 
rough but I think it could be a nice addition to the Isabelle Library with 
some more work, mostly for Imperative_HOL (~~/src/HOL/Imperative_HOL) which 
can only store values of countable types in its heap.


However, as Lukas Bulwhan said to me, improving it and integrating it in 
Isabelle while nobody use it would certainly be a lost of time.


So here is my question: would anybody be interested in this addition ?

I attach this library with a theory containing tests/examples.

Anyway, if you have some advices for improving it, they would be welcome.

Regards,

Mathieu Giorgino


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

Re: [isabelle-dev] NEWS - Redundant lemmas

2011-09-22 Thread Peter Lammich


 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 to get their theories working, and then
 work gradually to eliminate the dependencies on it. What do you think?
 

In Java, there is a deprecated flag for such issues. Isabelle could
then issue
a warning whenever using a deprecated lemma --- like the legacy-warnings
it already issues when using some deprecated features (recdef, etc.)


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

[isabelle-dev] JinjaThreads in French!

2012-02-02 Thread Peter Lammich

... 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/mailman/listinfo/isabelle-dev

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

2012-02-14 Thread Peter Lammich

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] Invoking Simplifier inside simproc, ### Simplifier: renamed bound variable

2012-03-26 Thread Peter Lammich

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 t=t' and returns it
as simplification lemma.

I tried to follow the approach done in the cancellation simprocs,
getting something like:

  fun assn_simproc_fun ss credex = let
val ctxt = Simplifier.the_context ss
val ([redex],ctxt') = Variable.import_terms true [term_of credex]
  ctxt;
val export = singleton (Variable.export ctxt' ctxt)

fun do_transform t = [...]

val new_form = do_transform redex;

val result = Option.map (export o mk_meta_eq)
  (Arith_Data.prove_conv_nohyps
[simp_tac (HOL_basic_ss addsimps @{thms star_aci}) 1] ctxt
(redex,new_form)
  );

  in result
  end;

Where do_transform does the job of transforming the term.
However, I get strange warning messages starting with 
### Simplifier: renamed bound variable ..., I guess from the inner
call to the simplifier. When tracing the value of redex, I find that
it may contain loose bound variables, and the warnings from the
simplifier seem to be related to redex containing loose bound vars. 

Now my question: Are these renamed bound variable - messages from the
simplifier harmful? What am I doing wrong, and how to do it properly?

Best and thanks in advance for any help,
  Peter



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

Re: [isabelle-dev] - and --

2012-04-17 Thread Peter Lammich


 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 test it and report problems in the usual 
 testing stage before the release.


I guess most of the PG users work on the release version, and would be
quite annoyed if the next release contains a buggy PG.


Peter


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

Re: [isabelle-dev] - and --

2012-04-17 Thread Peter Lammich

 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 test it and report problems in the usual 
 testing stage before the release.


I guess most of the PG users work on the release version, and would be
quite annoyed if the next release contains a buggy PG.

Peter



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

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

2012-05-08 Thread Peter Lammich

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 constructors on purpose.  (I can dig up an email 
  by
  Elsa Gunter from the late 1990-ies, if you want.)
 
  It is precisely such a convincing example I am looking for. It seems to me
  that such constraints restrict the types artificially: the type makes sense
  without it. What is gained by the constraint?
  
  Foundationally nothing, which is why constraints are not present in most of 
  the
  raw definitional primitives, at the bottom of the logic.
  
  There is a difference of the foundation vs. the user context, though. (As 
  usual
  user means other packages or end-users connected to the surface syntax of 
  such
  packages.) The Isabelle experts in the background have spent countless 
  years to
  make all this work most of the time, such that it is rarely visible now 
  where
  things actually happen, and how.
 
 Kudos to the experts, but my question was *why* the type constraints are
 supported for dataypes. What is the use case?

One use case arises in imperative HOL, where you want to declare
datatypes that can be stored on the heap, and thus, they only make sense
if constrained to ::heap - sort. E.g.


datatype a'::heap linked_list = nil | node 'a 'a linked_list ref

Currently, Imperative/HOL does some ML-magic after the datatype
declarations here, which certainly looks much cleaner when just adding a
sort constraint.

Peter

 
 Tobias
 
  
  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

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

2012-07-17 Thread Peter Lammich

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 to implement such a feature?

Example:

locale l =
  fixes g::'a = 'b
begin
  definition foo x == (g x,x)
  lemma lem: snd (foo x) = x unfolding foo_def by simp
end

interpretation i: l id .
thm i.lem
export_code i.foo
*** Not a constant: l.foo id


What I would like here is, that the interpretation command introduces a
new constant i.foo, with the definition (or at least code equation)
i.foo x == (g x,x), and that this constant is also used in the
instantiated facts.

For this, the code generator could then generate code.

Currently, I am defining those constants by hand, after the
interpretation, which causes lots of boilerplate in my real applications
with more than a dozen of definitions.


-- Peter


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

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

2012-08-03 Thread Peter Lammich

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 separate document, re-using the
tex-files generated by the previous run of Isabelle.  


Peter


On Fr, 2012-08-03 at 09:05 +0200, Jasmin Christian Blanchette wrote:
 Am 02.08.2012 um 23:20 schrieb Makarius:
 
  BTW, there were other specialities in Collections, Refine_Monadic, and also 
  Huffman concerning document generation. These were rather unexciting, and 
  easily performed by regular system functions.
 
 For Huffman, the fixdoc script is not critical. It replaces 'a with \alpha 
 and things like that. I can live without it. But what do you mean by regular 
 system functions?
 
 Jasmin
 
 ___
 isabelle-dev mailing list
 isabelle-...@in.tum.de
 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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

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

2012-08-03 Thread Peter Lammich


 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 shorter 
 than the ruby stuff.


I hope there is no need. I'm currently working on that issue (and some
related restructuring of the ICF), but it may take some time, as the ICF
and its dependencies are quite large, and my modifications are by far
not backward compatible.


This ruby-script was build as a quick hack to solve the problem of
instantiating generic algorithms for all possible combinations of
implementations. I'm not yet sure what a good solution would be, or
whether one should avoid these instantiations at all, as they seem to be
rarely needed.


Peter


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

Re: [isabelle-dev] superfluous [?]

2012-10-10 Thread Peter Lammich

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, but when building the session via command line it
computes for 10 minutes and then fails ...

Peter

On Mi, 2012-10-10 at 17:52 +0200, Makarius wrote:
 On Wed, 10 Oct 2012, Ondřej Kunčar wrote:
 
  This problem refers to 3fc6b3289c31.
 
  If I type in this simple formalization
 
  lemma c: x = x
  by metis
 
  thm c
 
  the following theorem is printed ?x = ?x  [?]. What is that suspicious 
  question mark? It seems to be produced by any metis call. And it is 
  reproducible almost always.
 
 This is the normal result of printing Thm.status_of in the traditional 
 way.  It is now getting in the way, because terminal proofs ('by') are 
 always parallel in Isabelle/jEdit.
 
 I am about to rework this critical kernal status information, but it 
 requires some more thinking.  Last time I changed something there, it was 
 immediately reported as problem that fewer [!] were printed as before.
 
 
   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] NEWS: more informative errors in lazy enumerations

2012-10-17 Thread Peter Lammich

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 trace buffer when
debugging tactics.


 Side remark:
 
 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 should now work without 
 it, just by letting 'qed' crash and looking at the error message.  Of 
 course, 'apply' has other uses and is not affected here.

I never knew it, but already got many questions from students whether
such a command exists, and I always denied it.


Peter


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

[isabelle-dev] Resolve with premises

2013-01-18 Thread Peter Lammich

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. Should
we? Opinions?

Peter


---

ML {*
  (* Resolve with premises. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprems_tac ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal, i)
=
  let
fun non_atomic (Const (==, _) $ _ $ _) = true
  | non_atomic (Const (all, _) $ _) = true
  | non_atomic _ = false;

val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule 
  (singleton (Variable.export ctxt' ctxt)) goal';
val Rs = filter (non_atomic o Thm.term_of) 
  (Drule.strip_imp_prems goal'');

val ethms = Rs | map (fn R =
  (Raw_Simplifier.norm_hhf (Thm.trivial R)));
  in eresolve_tac ethms i end
  );

(* Resolve with premise. Copied and adjusted from
Goal.assume_rule_tac. *)
fun rprem_tac n ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal,
i) =
  let
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
val goal'' = Drule.cterm_rule 
  (singleton (Variable.export ctxt' ctxt)) goal';

val R = nth (Drule.strip_imp_prems goal'') (n - 1)
val rl = Raw_Simplifier.norm_hhf (Thm.trivial R)
  in
etac rl i
  end
  );

  val setup =
  Method.setup @{binding rprems} 
(Scan.lift (Scan.option Parse.nat)  (fn i = fn ctxt = 
  SIMPLE_METHOD' (
case i of
  NONE = rprems_tac ctxt
| SOME i = rprem_tac i ctxt
  ))
) 
Resolve with premises



*}

setup setup


(* EXAMPLES: *)


lemma \lbrakk A\LongrightarrowB; B\LongrightarrowC; A \rbrakk
\Longrightarrow C
  apply (rprems 2) -- Explicitely specify number of premise
  apply (rprems 1)
  .

lemma \lbrakk A\LongrightarrowB; B\LongrightarrowC; A \rbrakk
\Longrightarrow C
  apply (rprems) -- Resolve with any matching premise, 
first to last, backtracking
  apply (rprems)
  .

--


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

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

2013-07-18 Thread Peter Lammich

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
matching target-language keywords, etc).

--
  Peter

On Do, 2013-07-18 at 15:03 +0200, Florian Haftmann wrote:
  This crash happens in Isabelle/38466f4f3483, e.g. on Mac OS X:
  
  HOL-Codegenerator_Test FAILED
  (see also
  /Volumes/Macintosh_HD/Users/makarius/.isabelle/heaps/polyml-5.5.1_x86-darwin/log/HOL-Codegenerator_Test)
  
  
  ROOT.scala:696: warning: Class Generated_Code$Pattern differs only in
  case from Generated_Code$pattern. Such classes will overwrite one
  another on case-insensitive filesystems.
  final case class Pattern() extends pattern
  ...
  *** Code check failed for SML: $ISABELLE_PROCESS -r -q -e 'datatype
  ref = datatype Unsynchronized.ref; use ROOT.ML handle _ = exit 1' Pure
  *** At command export_code (line 19 of
  ~~/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy)
  Unfinished session(s): HOL-Codegenerator_Test
 
 Interestingly, the code generator test for Scala (which indeed is
 brittle on case-insensitive file systems) gives a warning but seems to
 succeed.  What really fails is the SML test which is not sensitve
 towards case-insensitive file systems.  Does this also occur on other
 platforms?
 
   Florian
 
 ___
 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] Advice for replacing @{simpset} with @{context}.

2013-09-13 Thread Peter Lammich


 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 context, using
 simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
 old tools by making them depend on (ctxt : Proof.context) instead of
 (ss : simpset), then turn (simpset_of ctxt) into ctxt.
 


So the only way to replace a HOL_basic_ss addsimps ... somewhere deep
inside my code (in my actual case, inside a conversion) is to thread
through the proof context everywhere? ... a quite tedious change.


--
  Peter


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

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

2013-09-19 Thread Peter Lammich

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, everything works as expected.

It looks like (see also my previous post) that monad-syntax has some
severe issues with abbreviations, that I would really like to see fixed
in the next release, as they render unusable many of my tools.

--
  Peter

theory Scratch
imports 
  ~~/src/HOL/Library/Monad_Syntax
begin

abbreviation abbr1 == Some () = (%_. Some False)

abbreviation abbr2 == do {
Some ();
Some False
  }

(* ### Additional type variable(s) in specification of abbr2: 'a *)

term (abbr1, abbr2)

(*
(Some () = (%_::unit. Some False),
  %TYPE::unit itself. Some () = (%_::unit. Some False))
  :: bool option * (unit itself = bool option)
*)


definition abbr3 == do {
Some ();
Some False
  }

(* No additional type parameter *)


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

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

2013-09-20 Thread Peter Lammich


 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://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2013-09-26 Thread Peter Lammich

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 folder does not contain all necessary files, on
startup, isabelle tells me:

Unknown logic HOL -- no heap file found in:
  /home/lammich/.isabelle/Isabelle_25-Sep-2013/heaps/polyml-5.5.1_x86-linux
  /home/lammich/opt/Isabelle_25-Sep-2013/heaps/polyml-5.5.1_x86-linux


Best,
  Peter



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

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

2013-09-26 Thread Peter Lammich

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 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 folder does not contain all necessary files, on
 startup, isabelle tells me:
 
 Unknown logic HOL -- no heap file found in:
   /home/lammich/.isabelle/Isabelle_25-Sep-2013/heaps/polyml-5.5.1_x86-linux
   /home/lammich/opt/Isabelle_25-Sep-2013/heaps/polyml-5.5.1_x86-linux
 
 
 Best,
   Peter
 
 
 
 ___
 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] Testboard

2013-09-27 Thread Peter Lammich

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
reasonable time?


--
  Peter

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

Re: [isabelle-dev] Testboard

2013-09-27 Thread Peter Lammich

I always thought that there are two use-cases of Testboard:
  1. Whenever you push to the Isabelle repository, this is tested by
testboard
  2. You can push your changeset only to testboard, to check it before
pushing it to the isabelle repo and perhaps breaking it.

However, according to Lars' reply, the second use-case is almost not
possible, as a particular changeset will quickly be hidden by a huge
number of later pushes to the isabelle repository, and never be touched
again.

So here is my question:
  If I have some changeset, and want to check whether it breaks AFP
before pushing 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 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
  reasonable time?
 
 Basically Mira is just watching the repository. If a test run finishes, 
 it looks at the repository, takes the tip and tests it (if it was not 
 already tested). In particular, this means that later pushes can take 
 the focus away from your pushes.
 
 It might be a good idea to implement a strategy which tests the existing 
 heads in reverse chronological order (commits pushed last get tested 
 first), but I am not sure whether this information is available in 
 Mercurial (we have the commit date, but this is not necessarily related 
 to the push-date).
 
-- Lars
 ___
 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] Concerning AFP 2a0f81020af9

2013-10-31 Thread Peter Lammich

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.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-October/004787.html



 
 What is »the snapshot« in this context?  The develepment snapshot on
 http://afp.sourceforge.net/download.shtml is volatile.
 
   Florian
 


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

Re: [isabelle-dev] Isabelle2013-2 release

2013-11-21 Thread Peter Lammich

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, schrieb Makarius:
  Are there any other potential problems of Isabelle2013-1 that were not 
  reported
  yet?
 
 There is a problem with autoquickcheck in Isabelle/jedit. It sometimes fails 
 to
 find or dislay a counterexample. I have a theory with a wrong lemma in it. 
 When
 I load the theory, no counterexample is displayed. When I edit the theory such
 that that lemma needs to be rechecked, suddenly the counterexample is found.
 Afterwards it is always found reliably. The first time is the difficult time.
 
 This is not easy to reproduce: if you just use False or x=x, it will find 
 a
 counterexample reliably. I have tried to create a short example but failed. I
 have noticed this some time ago, but was never sure if it was just a fluke. 
 Now
 I have a collection of theories where it reproduces reliably.
 
 Tobias
 ___
 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] Isabelle2013-2 release

2013-11-21 Thread Peter Lammich

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 thus look 
 finished, although the state is failed.  (This bad state is not rendered 
 specifically, because it is not supposed to happen.)

On my machine, there is also a second way to run into this Problem:
  Just load a theory with a diverging command, and wait long enough
  (nondeterministically, between tens of seconds and several minutes). 
  The command appears to finish, and the theorem's status is failed.


In an earlier message on this thread, you have posted a patch. However,
I cannot apply this patch to the development repository, nor does the
revision db3d3d99c69d, which your patch refers to, exist.

So how and against what should I apply this patch?

--
  Peter

 
 This means that it is hardly possible to edit serious proof developments 
 reliably in Isabelle/jEdit.
 
 
 The problem is going back to Isabelle/78693e46a237 (03-Sep-2013), which is 
 just at the start of the consolidation of a whole summer's work.
 
 In Isabelle/88c6e630c15f (24-Sep-2013) the change of command spans for the 
 sledgehammer panel has exposed the dormant problem in a way that it 
 becomes apparent very easily.  (Thus the sledgehammer change did not 
 introduce it, as I've first thought.)
 
 
 I am a little disturbed that such a serious problem was undetected (or 
 unreported) for such a long time.  It shows that the Isabelle development 
 and release process no longer works reliably -- although I've spent about 
 the same time doing new things in summer versus getting the release ready 
 in autumn.
 
 Another conclusion is that the majority of serious proof development is 
 still done in Proof General.
 
 
   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] Isabelle2013-2 release

2013-11-21 Thread Peter Lammich

Finally, here is another way how isabelle-release/5adc68deb322 (i.e.
after your first patch)
appears to have proven a non-theorem.
Load the following and just wait a moment until the tactic interrupts
due to stack-overflow. The theorem's status gets failed, but this is not
displayed in isabelle/jEdit, nor is there an error on the tactic-block.

I think that is a clear indication that the status failed can happen
(stack-overflow, out-of-memory, what-so-ever), and should be displayed
in isabelle/jEdit!


  ML {*
fun stack_overflow a = a + 1 + stack_overflow a
  *}

  lemma f:False 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 a theory with a diverging command, and wait long enough 
  (nondeterministically, between tens of seconds and several minutes). The 
  command appears to finish, and the theorem's status is failed.
 
 I would guess that it is just another way to get edits applied eventually. 
 There are many timers in Isabelle/jEdit and the underlying Isabelle/Scala 
 infrastructure, e.g. for garbage collection of unused document versions.
 
 This is a highly interactive computer-game.  The first time in the history 
 of ITP that interaction really happens.
 
 
  In an earlier message on this thread, you have posted a patch. However, 
  I cannot apply this patch to the development repository, nor does the 
  revision db3d3d99c69d, which your patch refers to, exist.
 
 This mail thread is about the release: 
 https://bitbucket.org/isabelle_project/isabelle-release
 
 
   Makarius


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

Re: [isabelle-dev] Isabelle2013-2 release

2013-11-21 Thread Peter Lammich


 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.Interrupt?
According to my experience, there are no such methods, so fixing this
problem may not be that urgent.

--
  Peter



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

Re: [isabelle-dev] Isabelle2013-2 release

2013-11-21 Thread Peter Lammich

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/5adc68deb322 (i.e.
 after your first patch)
 appears to have proven a non-theorem.
 Load the following and just wait a moment until the tactic interrupts
 due to stack-overflow. The theorem's status gets failed, but this is not
 displayed in isabelle/jEdit, nor is there an error on the tactic-block.
 
 I think that is a clear indication that the status failed can happen
 (stack-overflow, out-of-memory, what-so-ever), and should be displayed
 in isabelle/jEdit!
 
 
   ML {*
 fun stack_overflow a = a + 1 + stack_overflow a
   *}
 
   lemma f:False 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 a theory with a diverging command, and wait long enough 
   (nondeterministically, between tens of seconds and several minutes). The 
   command appears to finish, and the theorem's status is failed.
  
  I would guess that it is just another way to get edits applied eventually. 
  There are many timers in Isabelle/jEdit and the underlying Isabelle/Scala 
  infrastructure, e.g. for garbage collection of unused document versions.
  
  This is a highly interactive computer-game.  The first time in the history 
  of ITP that interaction really happens.
  
  
   In an earlier message on this thread, you have posted a patch. However, 
   I cannot apply this patch to the development repository, nor does the 
   revision db3d3d99c69d, which your patch refers to, exist.
  
  This mail thread is about the release: 
  https://bitbucket.org/isabelle_project/isabelle-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

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

2013-12-03 Thread Peter Lammich

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 einem Absturz(welche übrigens seit 
 neuestem recht häufig vorkommen) mein File beschädigt und kann es nicht mehr 
 öffnen bzw. zeigt es als leer an. Ich habe das korrupte File angehängt, 
 vielleicht trägt es ja zur Fehlerfindung/-behebung bei.
 Woran kann das liegen, dass Isabelle bei mir so häufig abstürzt(ca. einmal 
 alle zwei Stunden)? (Ich habe Windows 8.1 und einen neuen Laptop)


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

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

2014-01-13 Thread Peter Lammich


 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 change to hypsubst! (Having thought
of doing this patch myself several times, not knowing about the older
discussion on this list ;) )

--
  Peter



 All comments welcome,
  Thomas.
 
 
 
 
 The information in this e-mail may be confidential and subject to legal 
 professional privilege and/or copyright. National ICT Australia Limited 
 accepts no liability for any damage caused by this email or its attachments.
 ___
 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] Remaining uses of Proof General?

2014-04-28 Thread Peter Lammich

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 on the meaningless parts of the file
directly after the point where I am editing. I'm not even convinced that
it is the right approach to let Isabelle/jEdit's heuristics decide when
and what it processes, and make user intervention impossible at first
place (Or even worse, force the user into workarounds like inserting
semicolons or ends behind the current editing point, which seems to be
common practice among Isabelle/jEdit users)

2. In PG, when the processed region reaches the end of a theory file, I
can be pretty sure that everything is fine with this theory. In
Isabelle/jEdit, I have to scan the theory status panel manually for
remaining red or pink bars, which is very inconvenient for large
projects with hundreds of files.

Moreover, I find it a bit scary that severe errors related to
Isabelle/jEdit's document processing model (cf.
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00170.html)
can go undiscovered for several month, although most Isabelle users are
on Isabelle/jEdit these days. I ask myself: Have they got so used to
strange behaviours of the IDE that they do not realize severe errors any
more?


--
  Peter





On Mo, 2014-04-28 at 09:14 +0200, Andreas Lochbihler wrote:
 Hi Makarius,
 
 Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle 
 time (and 
 ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great 
 when it comes to 
 working on small projects or refactoring existing sources. I really like the 
 negative line 
 spacing setting and completion of fact names! Thanks!
 
 My main usage of PG is when I want to construct a complicated proof method 
 call like
 
 (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... 
 simp del: ...)+
 
 that collapses an apply script of a hundred lines. I haven't yet found a 
 convenient way to 
 write the apply script in Isabelle/jEdit, because of reactivity issues (see 
 item 2 below) 
 and the continuous updates of the output window (when I scroll to some other 
 part of the 
 apply script using the cursor keys). Are there key bindings for scrolling 
 that do not move 
 the cursor?
 
 
 Here are some things that could be improved in Isabelle/jEdit (I am currently 
 on 
 Isabelle/4e2a0d4e7a82):
 
 1. Symbol completion in PG was absolutely deterministic. The immediate symbol 
 completion 
 in jEdit works great, too, I merely had to learn new sequences of key 
 strokes. Symbol 
 completion of non-unique results is not satisfactory.
 
 a) Given some text like
 
 definition foo where foo = ...
 
 when I add an attribute like [simp]: after the where, I get a symbol 
 completion popup to 
 replace the : with the element sign. Usually, my next thing is to move the 
 cursor with the 
 cursor keys. But the popup gobbles all the key strokes until I explicitly 
 close it with 
 ESC. As colons are used everywhere in Isabelle's outer syntax, it would 
 really be great if 
 the popup only appears when I am in inner syntax.
 
 b) Sometimes, when I write a HOL term, I used to not get the completion popup 
 when I enter 
 something like \un if there were sufficiently many parse errors in that 
 partial term. Even 
 Ctrl-b did not help. However, I cannot reproduce it in a small example at the 
 moment.
 
 
 2. Reactivity when processing large files
 
 With PG, I knew how to control the Isabelle prover. When I edit a large file 
 in a larger 
 project like JinjaThreads, every now and then, Isabelle changes the 
 background colour from 
 red to gray and then, apparently nothing happens for minutes before Isabelle 
 turns it red 
 again and starts reprocessing. Is there some way to explicitly tell Isabelle 
 that it 
 should now start to check again. Toggling continuous checking does not 
 help. Sometimes, 
 I even have to close the theory file and reopen it again.
 
 
 3. Navigation between theories files
 
 In PG, I usually have only a small subset of the loaded theories and ML files 
 open as 
 buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I 
 use Ctrl-` to 
 go to the previous file, but going to a different one is a pain, because I 
 have to search 
 it in the complete list of open files.
 
 It would be great if there was a list of just those files that I had on my 
 screen 
 previously, not all loaded files.
 
 Moreover, when I close a file and then press Ctrl-` in the file that shows 
 up, I do not 
 get to the file I have visited before the two, but to some arbitrary other. 
 Can jEdit 
 remember the order in which files have been visited? XEmacs at least does 
 this.
 
 
 Maybe there are already solutions to the above annoyances, I just don't know

[isabelle-dev] AFP: Failing entries

2014-06-25 Thread Peter Lammich

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.sourceforge.net/status.shtml
is 3 days old. When will this be updated?

--
  Peter


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

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

2014-06-26 Thread Peter Lammich

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 thy-file)

I have compiled a list of problems that I encountered during my work.
I have added descriptions to how PG solved these problems.

The problem report here refers to Isabelle version 2ccd6820f74e.

My overall impression is that Isabelle/jEdit is usable but much less
mature than PG:
It does not scale well to large projects, and tends to be unstable.
It has many cool advanced features, but lacks important basic ones. 

However, in my opinion, Isabelle/jEdit is approaching a level of
maturity required for production use, once the user knows about its
deficits and how to avoid them. I will continue using Isabelle/jEdit for
a few more weeks, hoping that a few more basic features will be
added/fixed before the next release ...


SCALABILITY  STABILITY:

* Isabelle/jEdit gets really slow and unresponsive when many files are
loaded (you have to wait seconds for a keystroke to show its effect). As
all prerequisite theories (not in an image) are automatically loaded,
this is unavoidable. In PG, it's no problem to load a theory with many
prerequisites, nor to have many buffers open simultaneously. 

NOTE: This problem could be solved in my case by 1) giving jEdit a
ridiculously large amount of heap space (4Gb) and, 2) using images for
prerequisite theories.

* Isabelle/jEdit does not scale to large files. Error markers on the
right side are only displayed for a context around the current cursor
position. There seems to be no way to jump to the error position. If the
error happens to be displayed as a red bar on the right side of the
editor area, pixel-accurate mousing is required to jump to the error,
and not to a position dozens of lines away.   

In PG, you could always jump to the position where processing failed by
Ctrl-. . Moreover, you got error messages with file names and line
numbers, that you could use to navigate to the error position easily.

* Isabelle/jEdit seems to be quite unstable. Within one week, it
happened several (3 or 4) times that the whole thing just became
unresponsive, and had to be restarted to continue work. In PG, those
things happen perhaps once in a month.

IMPORTANT FEATURES THAT ARE MISSING  OVERLY TEDIOUS WORKFLOWS

* Isabelle/jEdit does not support highlighting of paranthesis in the
output window (it does work in PG!). This is an essential feature to
read bigger goal states. 

Moreover, the output buffer does not support middle-mouse-button
copy-and-paste on my ubuntu-box, while it perfectly works in the editor
window.

* 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.
This feature is a real flow-stopper when exploring proofs. 

In PG, it is possible to have separate buffers for the goal-state, the
tracing, and the warning messages, thus you always see the current
subgoal you are working on without scrolling down some buffer every
time.

* If sledgehammer (both over panel and as command) is running, further
processing of the file is blocked/very slow. Thus, it is not possible
to run sledgehammer and, in parallel, continue exploration to find your
own proof. In PG, parallel sledgehammering works, and I used it
extensively. In Isabelle/jEdit I now think twice before I invoke
sledgehammer, because it just interrupts my workflow and I have to wait
for it to finish staring at the sledgehammer-window and doing nothing. 


* Isabelle/jEdit cannot open a theory-file without processing it. This
is in particular a problem when porting stuff and opening the original
version of the same file to look something up. Even worse: Once opened,
you cannot close the file again, and it will remain in the theory panel
(with an error marker) until you quit jEdit.

In PG, it is no problem to open a file without processing it.

* The standard search (Ctrl-F) function does not allow to enter
non-ASCII characters at all. This is a real show-stopper if you search
for a text containing such characters. In PG, you could at least use
\... - tokens to enter non-ASCII characters.

Moreover, I would like an incremental search, but there is probably a
jEdit pluging somewhere? (Probably with the same problems of entering
non-ASCII characters)


* When theories have inconsistent file/theory name, you will only find
the error by stepwise going back the chain of bad theory -  errors,
file by file. This is simply tedious. In PG, you got a backtrace in the
output, and could immediately identify the broken file.


* Auto-Completion does not really work. You have to decide for a
completion delay. If you choose it too short, some completions will
not appear at all. If you

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

2014-06-27 Thread Peter Lammich


 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 output panel display the error
message, or get a tooltip on the error message, without *first* locating
its position in the editor window!?

Following example: Slightly change the simpset, and try to load
$AFP/Automatic_Refinement/Lib/Misc.thy, a 4400 lines beast. Change the
simpset so that it fails somewhere in the middle of the theory.
I only see a red mark in the theory-panel, but how do I navigate to the
error location?

In PG, I actually saw file-name/line-number/error-message. In
Isabelle/jEdit, the only way I know is to open the file, hope that the
text-overview column displays the error already, and try a precise
mouse-click to get to the location. If the error-column does not display
the error, because it is not within the limit, I have to scroll through
the file manually.

So am I missing some feature here that makes the workflow 
Navigate to an error in a theory file
simpler?


--
  Peter

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

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

2014-06-27 Thread Peter Lammich


 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 should describe what 
 really happens, with clear experimental setup.

Giving a clear experimental setup is a real problem for errors that
appear nondeterministically.



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

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

2014-06-27 Thread Peter Lammich

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.
  This feature is a real flow-stopper when exploring proofs.
 
  In PG, it is possible to have separate buffers for the goal-state, the
  tracing, and the warning messages, thus you always see the current
  subgoal you are working on without scrolling down some buffer every
  time.
 
 Just a few hints:
 
* Regular messages (writeln, warning, error) also appear in the
  squiggly rendering of the sources, to be hovered over and inspected
  without scrolling *the* Output.  There is in fact no reason to have
  just one (or two or three) focal points for certain printed results,
  like in TTY / PG.
 
* Tracing is a different topic -- it was never really sorted out
  satisfactorily in the history of PG.  More than 1 year ago, Lars Hupel
  made some efforts for modernized tracing in PIDE, but it got seriously
  encumbered by PG legacy.  It still needs to be revisited just before
  the Isabelle2014, to see if it can be made ready for prime time.
 
 I don't see any show-stoppers here.  Just more potential for refinements, 
 when PG is discarded.


These hints do not adress the problem! During proving, I want to see the
goal state in first place, not the errors/warnings/etc. If I have to use
the mouse and scroll down to the goal state every time I change
something, this really interrupts the working flow during proof
development. 

Once I have finished the proof, I am interested in the error and warning
messages, and really appreciate the tooltips on the squiggly lines.

--
  Peter



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

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

2014-06-27 Thread Peter Lammich

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 nondeterministically.
 
 The first thing is to describe the starting conditions:
 
* Precise CPU model + memory size
vendor_id   : GenuineIntel
cpu family  : 6
model   : 42
model name  : Intel(R) Core(TM) i7-2720QM CPU @ 2.20GHz
stepping: 7
microcode   : 0x1a
cpu MHz : 2194.940
cache size  : 6144 KB
physical id : 0
siblings: 8
core id : 0
cpu cores   : 4
apicid  : 0
initial apicid  : 0
fpu : yes
fpu_exception   : yes
cpuid level : 13
wp  : yes
flags   : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov
pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx
rdtscp lm constant_tsc arch_perfmon pebs bts rep_good nopl xtopology
nonstop_tsc aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est
tm2 ssse3 cx16 xtpr pdcm pcid sse4_1 sse4_2 x2apic popcnt
tsc_deadline_timer aes xsave avx lahf_lm ida arat epb xsaveopt pln pts
dtherm tpr_shadow vnmi flexpriority ept vpid
bogomips: 4389.88
clflush size: 64
cache_alignment : 64
address sizes   : 36 bits physical, 48 bits virtual
power management:

+

8Gb of memory, 8Gb of swap space

 
* Operating system
Distributor ID: Ubuntu
Description:Ubuntu 12.04.4 LTS
Release:12.04
Codename:   precise

 
* ML options (heap size, threads)
 

ML_IDENTIFIER=polyml-5.5.2_x86-linux
POLYML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2
ML_SYSTEM=polyml-5.5.2
ML_PLATFORM=x86-linux
ML_OPTIONS=-H 500
ISABELLE_POLYML=true

* JVM options (heap size)
JEDIT_JAVA_OPTIONS=-Xms2048m -Xmx4096m -Xss4m

I also attached the output of isabelle getenv -a


 
 The second thing to point the the examples that were used, and give some 
 hints about the concrete situation.

I will try to remember those if it occurs next. 

By the way, another Isabelle/jEdit user at our chair pointed out a
workaround if things seem to be frozen: Just go the beginning of the
current file and make a change there ... this usually wakes up the IDE
again.


--
  Peter


LC_PAPER=de_DE.UTF-8
ISABELLE_TMP_PREFIX=/tmp/isabelle-lammich
CVC3_REMOTE_SOLVER=cvc3
SSH_AGENT_PID=1991
LC_ADDRESS=de_DE.UTF-8
LC_MONETARY=de_DE.UTF-8
ISABELLE_ATP=/home/lammich/devel/Isabelle-devel/src/HOL/Tools/ATP
ML_IDENTIFIER=polyml-5.5.2_x86-linux
ISABELLE_FONTS=/home/lammich/devel/Isabelle-devel/lib/fonts/IsabelleText.ttf:/home/lammich/devel/Isabelle-devel/lib/fonts/IsabelleTextBold.ttf
JEDIT_HOME=/home/lammich/devel/Isabelle-devel/src/Tools/jEdit
Z3_NEW_SOLVER=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1/x86_64-linux/z3
GPG_AGENT_INFO=/tmp/keyring-my6CuJ/gpg:0:1
JEDIT_SYSTEM_OPTIONS=-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true 
-Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle
MIRABELLE_THEORY=Main
EXEC_PROCESS=/home/lammich/.isabelle/contrib/exec_process-1.0.3/x86_64-linux/exec_process
KODKODI_PLATFORM=x86-linux
SHELL=/bin/bash
TERM=xterm
ISABELLE_BUILD_JAVA_OPTIONS=-Xmx1024m -Xss1m
XDG_SESSION_COOKIE=e98a42690e78d743ed7935360007-1403084616.517570-346887857
ISABELLE_IDENTIFIER=
ISABELLE_COMPONENTS_MISSING=
ISABELLE_JDK_HOME=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux
ISABELLE_MAKEINDEX=makeindex
Z3_NEW_HOME=/home/lammich/.isabelle/contrib/z3-4.3.2pre-1/x86_64-linux
ISABELLE_PROCESS=/home/lammich/devel/Isabelle-devel/bin/isabelle_process
Z3_NEW_INSTALLED=yes
ISABELLE_JAVA_EXT=/home/lammich/.isabelle/contrib/jdk-8u5/x86_64-linux/jre/lib/ext
LC_NUMERIC=de_DE.UTF-8
WINDOWID=67827196
ISABELLE_DOCS_RELEASE_NOTES=ANNOUNCE:README:NEWS:COPYRIGHT:CONTRIBUTORS:contrib/README:README_REPOSITORY
MIRABELLE_TIMEOUT=30
GNOME_KEYRING_CONTROL=/tmp/keyring-my6CuJ
ISABELLE_BIBTEX=bibtex
DVI_VIEWER=xdg-open
Z3_REMOTE_SOLVER=z3
REPLY=
ISABELLE_SETTINGS_PRESENT=true
ISABELLE_BUILD_OPTIONS=
MUTABELLE_IMPORT_THEORY=Complex_Main
POLYML_HOME=/home/lammich/.isabelle/contrib/polyml-5.5.2
Z3_COMPONENT=/home/lammich/.isabelle/contrib/z3-3.2-1
GTK_MODULES=canberra-gtk-module:canberra-gtk-module
ISABELLE_PLATFORM_FAMILY=linux
ISABELLE_SLEDGEHAMMER_MASH=/home/lammich/devel/Isabelle-devel/src/HOL/Tools/Sledgehammer/MaSh
ISABELLE_PATH=/home/lammich/.isabelle/heaps:/home/lammich/devel/Isabelle-devel/heaps
USER=lammich
ML_SYSTEM=polyml-5.5.2
LC_TELEPHONE=de_DE.UTF-8
LS_COLORS=rs=0:di=01;34:ln=01;36:mh=00:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:ca=30;41:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.lzma=01;31:*.tlz=01;31:*.txz=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.dz=01;31:*.gz=01;31:*.lz=01;31:*.xz=01;31:*.bz2=01;31:*.bz=01;31:*.tbz=01;31:*.tbz2=01;31:*.tz=01;31

Re: [isabelle-dev] AFP: Failing entries

2014-06-30 Thread Peter Lammich

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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] rtrancl lemma proposal

2014-10-01 Thread Peter Lammich

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 rtrancl_map:
   assumes ⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s
 and (x, y) ∈ r⇧*
   shows (f x, f y) ∈ s⇧*
   using rtrancl_sim[where S={(x,f x) | x. True}] assms 
   by simp blast

--
  Peter



On Mi, 2014-10-01 at 14:27 +0200, Christian Sternagel wrote:
 Dear developers,
 
 the following lemma seems like a basic fact about rtrancl:
 
 lemma rtrancl_map:
assumes ⋀x y. (x, y) ∈ r ⟹ (f x, f y) ∈ s
  and (x, y) ∈ r⇧*
shows (f x, f y) ∈ s⇧*
using assms(2, 1)
by (induct) (auto intro: rtrancl.rtrancl_into_rtrancl)
 
 I didn't find it in Main. Did anybody else ever use/need it? Is it 
 already part of some theory I did overlook? How about adding it?
 
 Caveat: It seems to be necessary to strongly instantiate it before usage.
 
 cheers
 
 chris
 ___
 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] How to activate/de-activate unifier-trace from ML-level

2014-11-03 Thread Peter Lammich

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.s.
Not sure whether this belongs to user or devel, but the reason 
for my message is  

http://sourceforge.net/p/afp/code/ci/7189f7ffd73e17c2395eb552c89004f5b8e0453e/ 

which seems to be related to tty-mode elimination that is currently
going on in dev-version.


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

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

2014-11-03 Thread Peter Lammich


 
 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 it, but at the end had to implement the hack in order to
get the desired behaviour.

Now you just removed the desired behaviour, not having a solution how to
get it back ... fortunately, in this particular case, it is not
essential, as this thing was inside some rarely used debugging tool.

--
  Peter



 
 
   Makarius
 
 
http://stop-ttip.org  777,443 people so far
 


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

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

2014-11-07 Thread Peter Lammich

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. But if a and b are numerals, this leads to a loop with
the
rewrite rule Divides.dvd_eq_mod_eq_0_numeral:

(numeral ?x dvd numeral ?y) = (numeral ?y mod numeral ?x = 0)

The enormous runtimes where due to this loop. It was not an infinite loop
because the simplifier has a depth limit.

Clearly, we cannot have such a loop. Either mod can use dvd or the other way
around, but not both.

Thanks for simp_trace_new/Lars Hupel, it made it easy to find out what was
going
on. [It would be nice if the trace could also show when the depth limit is
exceeded, it does not seem to].

Tobias

On 07/11/2014 17:45, Dmitriy Traytel wrote:
The culprit seems to be dvd_imp_mod_0 introduced as a simp rule in
773b378d9313.

The following takes again only 2 seconds.

declare dvd_imp_mod_0[simp del]
lemma prime(97::nat) by simp

Dmitriy

On 07.11.2014 15:31, Tobias Nipkow wrote:
Very nice observations, thank you. I was obviously too hasty to remove the
test which exposed this time leak. Once this issue has been fixed, I will
put
the long test back in, with a better comment.

Tobias

On 07/11/2014 15:27, Dmitriy Traytel wrote:
This is in Isabelle2014. In 229765cc3414 I make the same measurements as
Larry.
So indeed (as the text above those lemmas suggests) there seems to be a
regression with the simplifier setup.

Dmitriy

On 07.11.2014 15:10, Julian Brunner wrote:
The proof that 97 is prime only takes 1.3s on my machine (2.7 GHz i7),
with the whole theory Primes loading in about 4 seconds.

On Wed, Nov 5, 2014 at 8:37 PM, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
This theory takes quite a while to load, and I have found out why:

text{* A bit of regression testing: *}

lemma prime(97::nat) by simp
lemma prime(997::nat) by eval

The proof that 97 is prime takes 35 seconds on a very fast machine.
Can we
get rid of this or at least substitute a smaller number?
The question is whether this has really to be performed using simp.

As an alternative, a suitable code equations could be proven using the
primes_upto in Eratosthenes.thy, but I did never take any measurements
at which threshold the additional data structures outperform brute-force
calculation.

Florian

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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

Re: [isabelle-dev] Problem in the AFP

2015-03-21 Thread Peter Lammich

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


On Sa, 2015-03-21 at 18:08 +0100, Florian Haftmann wrote:
  isabelle: e6f0c361ac73 tip
  afp: 2a0dc69c001b tip
 
  Building LTL_to_GBA ...
  
  LTL_to_GBA FAILED
  (see also 
  /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/LTL_to_GBA)
  
= ('a, 'c) node_scheme set = ('a, 'c) node_scheme set
  Phase id_op
  Failed to identify: create_name_gba
  Failed to identify: ti_Lcnv
  0.048s elapsed time, 0.288s cpu time, 0.000s GC time
  ### theory LTL_to_GBA_impl
  ### 61.088s elapsed time, 341.092s cpu time, 22.988s GC time
  *** Failed to apply proof method (line 1156 of 
  /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy):
  *** goal (1 subgoal):
  ***  1. (?c,
  ***  %\phi.
  *** create_name_gba \phi =
  *** (%A. gba_to_idx A =
  ***  (%A'. stat_set_data_nres (card (frg_V A)) (card (frg_V0 
  A'))
  *** (igbg_num_acc A') =
  ***(%_. RETURN A'
  *** : \langleId\rangleltln_rel \rightarrow
  ***   \langleigbav_impl_rel_ext unit_rel nat_rel
  *** (\langleId\ranglefun_set_rel)\ranglenres_rel
  *** At command apply (line 1156 of 
  /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy)
  CAVA_buildchain1 CANCELLED
  CAVA_buildchain3 CANCELLED
  CAVA_LTL_Modelchecker CANCELLED
  Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1, 
  CAVA_buildchain3, LTL_to_GBA
  0:20:58 elapsed time, 0:59:35 cpu time, factor 2.84
 
 ___
 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] Reprocessing in Isabelle/jEdit

2015-03-24 Thread Peter Lammich

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 inside Isabelle/jEdit (f19f4afa49e2), it used to be so that 
 everything above was left alone. Now, if I edit a lemma in the middle of the 
 window, everything above it that is visible gets reprocessed. So if I write 
 something like
 
thm list.exhaust
 
 it can take a couple of seconds before I get feedback, if there’s some heavy 
 material preceding it. I noticed this behavior for the first time last week 
 or so — so did Mathias Fleury. We’re both using Macs.
 
 Is this behavior intentional? Is there a way to get the old, much more 
 responsive behavior back?
 
 Thanks.
 
 Jasmin
 
 ___
 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] Someone messed up HOL_library/Multiset_Order

2015-03-26 Thread Peter Lammich

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

*** Undefined fact: comm_monoid_diff_class.diff_cancel (line 302 of
~~/src/HOL/Library/Multiset_Order.thy)
*** At command by (line 302 of
~~/src/HOL/Library/Multiset_Order.thy)


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

Re: [isabelle-dev] Problem in the AFP

2015-03-23 Thread Peter Lammich

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
date:Fri Mar 13 15:42:00 2015 +0100
summary: adapting entries to new Deriving mechanism

in LTL_to_GBA-theory, this removes a linorder-constraint on
create_name_igba, which causes the breakdown, because later,
autoref is only given rules to refine create_name_igba for 
'a::linorder, but the respective lemmas do not repeat the
linorder-constraint. 

I fixed it by adding the linorder-constraint to the refinement, leaving
the abstract version general.

- definition create_name_igba :: 'a::linorder ltln \Rightarrow _ 
+ definition create_name_igba :: 'a ltln \Rightarrow _ where 


See now: changeset 56d43ce6541f

http://sourceforge.net/p/afp/code/ci/56d43ce6541f4602d390d1940ce69d211bd8724c/

--
  Peter

 
 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
 
 
 On Sa, 2015-03-21 at 18:08 +0100, Florian Haftmann wrote:
   isabelle: e6f0c361ac73 tip
   afp: 2a0dc69c001b tip
  
   Building LTL_to_GBA ...
   
   LTL_to_GBA FAILED
   (see also 
   /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/LTL_to_GBA)
   
 = ('a, 'c) node_scheme set = ('a, 'c) node_scheme set
   Phase id_op
   Failed to identify: create_name_gba
   Failed to identify: ti_Lcnv
   0.048s elapsed time, 0.288s cpu time, 0.000s GC time
   ### theory LTL_to_GBA_impl
   ### 61.088s elapsed time, 341.092s cpu time, 22.988s GC time
   *** Failed to apply proof method (line 1156 of 
   /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy):
   *** goal (1 subgoal):
   ***  1. (?c,
   ***  %\phi.
   *** create_name_gba \phi =
   *** (%A. gba_to_idx A =
   ***  (%A'. stat_set_data_nres (card (frg_V A)) (card (frg_V0 
   A'))
   *** (igbg_num_acc A') =
   ***(%_. RETURN A'
   *** : \langleId\rangleltln_rel \rightarrow
   ***   \langleigbav_impl_rel_ext unit_rel nat_rel
   *** (\langleId\ranglefun_set_rel)\ranglenres_rel
   *** At command apply (line 1156 of 
   /mnt/home/haftmann/data/afp/master/thys/LTL_to_GBA/LTL_to_GBA_impl.thy)
   CAVA_buildchain1 CANCELLED
   CAVA_buildchain3 CANCELLED
   CAVA_LTL_Modelchecker CANCELLED
   Unfinished session(s): CAVA_LTL_Modelchecker, CAVA_buildchain1, 
   CAVA_buildchain3, LTL_to_GBA
   0:20:58 elapsed time, 0:59:35 cpu time, factor 2.84
  
  ___
  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] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context

2015-04-02 Thread Peter Lammich


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 about local
contexts?

--
  Peter


 old-style global theory variants are
 available as Thm.global_ctyp_of and Thm.global_cterm_of.
 INCOMPATIBILITY.
 
 
 This refers to Isabelle/291934bac95e -- yet another step in the 
 localization project.
 
 There is a tiny semantic snag: both the local and global operations expand 
 abbreviations from the *global* background theory.  Mayne they should not 
 do anything like that at all, and leave changes to the types/terms to the 
 canonical check phases.  But that is another reform, another time.
 
 
 Hardly any values (thy: theory) should now show up in regular Isabelle/ML 
 tool implementations.  People who still think they don't understand proper 
 (ctxt: Proof.context) things, should practise more of the art of mental 
 abstraction -- and look at good examples in the Isabelle code base.
 
 
   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] NEWS: Thm.cterm_of and Thm.ctyp_of operate on local context

2015-04-02 Thread Peter Lammich


 
 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 confusion about what the real 
 context is.  

So what is the reason not to put it in more_thm.ML? 
There, it would not affect the kernel itself, and still appear as
Thm.cterm_of to the user.


--
  Peter



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

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

2015-05-28 Thread Peter Lammich

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




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

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

2015-09-15 Thread Peter Lammich

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

--
  Peter


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

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

2015-11-19 Thread Peter Lammich

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 test that everything still works?
> > 
> > I could do it, if nobody has objections.
> 
> I see no obstacles in going ahead.  What requires some thought is the
> material in ex/ directories is typically not assumed to be used in other
> sessions.  I have no idea wether these examples in Imperative-HOL where
> ever supposed to be used as libraries.
> 
> Cheers,
>   Florian
> 
> ___
> 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] Fwd: minor generalisation to Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to List_Sublist

2015-11-19 Thread Peter Lammich

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 message:
> > 
> > From: Peter Gammie 
> > Date: 15 November 2015 at 15:15:48 GMT
> > To: isabelle-dev@mailbroy.informatik.tu-muenchen.de
> > Subject: [isabelle-dev] minor generalisation to 
> > Imperative_HOL/ex/Imperative_Quicksort, rename Imperative_HOL/ex/Sublist to 
> > List_Sublist
> > 
> > Hi,
> > 
> > Can someone please apply the attached patch to Isabelle for me?
> > 
> > It does three things:
> > - generalises Imperative_Quicksort to work on linearly-ordered, 
> > heap-representable types, and not just nat
> > - renames Sublist to List_Sublist to avoid clashing with HOL/Library/Sublist
> > - mildly weakens the assumptions of lemma subarray_append in theory Subarray
> > 
> > The first may require existing theories to add type annotations. If this is 
> > a concern then perhaps the right thing to do is introduce new names for the 
> > polymorphic operations and preserve the existing ones, but I think that is 
> > overkill.
> > 
> > The second may also break existing theories but I do not know how to 
> > otherwise get around having two theories with the same name.
> > 
> > thanks,
> > peter
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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

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

2016-04-12 Thread Peter Lammich

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 variables for
> the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
> Thus terms like "f x" or "⋀x. P x" without any further syntactic context
> produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
> INCOMPATIBILITY, need to provide explicit type constraints for Pure
> types where this is really intended.
> 
> 
> This refers to Isabelle/b41c1cb5e251. After approx. 20 years in the 
> pipeline, the change came out rather small, but it required a few rounds 
> of empirical studies to get to this point.
> 
> I have already made a routine check of the places where the improvement 
> stage now produces a different result. This is included in the above 
> change. For AFP it is only 61a1c5a37227.
> 
> 
>   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] lifting syntax with proper symbols

2016-03-04 Thread Peter Lammich

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, depending on how much uncurried
functions or functions that return tuples you use, makes the difference
between nicely readable and completely unreadable relations.

--
  Peter



> 
> Ondrej
> 
> On 03/04/2016 12:36 PM, Andreas Lochbihler wrote:
> > Hi Makarius,
> >
> > How about LaTeX \Mapsto for ===>? This is what I use in my papers
> > following Ondrej and Brian's paper on lifting.
> >
> > I'd be happy to have syntax for ===> enabled by default, as it makes
> > transfer and parametricity rules much easier to read. I have no opinion
> > on --->.
> >
> > Andreas
> >
> > On 04/03/16 11:56, Makarius wrote:
> >> Isabelle2016 has removed quite a lot of old ASCII syntax, and made
> >> Isabelle symbols the
> >> default where old ASCII syntax is still available.
> >>
> >> A notable exception is lifting_syntax with its old-style ASCII-only
> >> notation, see
> >> http://isabelle.in.tum.de/repos/isabelle/annotate/aeee0a4be6cf/src/HOL/Transfer.thy#l19
> >>
> >>
> >> locale lifting_syntax
> >> begin
> >>notation rel_fun (infixr "===>" 55)
> >>notation map_fun (infixr "--->" 55)
> >> end
> >>
> >>
> >> I can imagine two reforms:
> >>
> >>* Use proper symbols for these operators (without keeping ASCII
> >>  replacement syntax).
> >>
> >>* Make the notation a global default, i.e. remove the locale and its
> >>  interpretations in applications.
> >>
> >>
> >> The usual question is which symbols are best.
> >>
> >> ===> appears to be more frequently used than --->. Based on that
> >> observation, the new
> >> triple-line arrow ⇛ could be used for ===>, and maybe a bold → for --->.
> >>
> >> This is only a first idea. There are many possibilities. It is also
> >> possible to add new
> >> glyphs to the Isabelle fonts, as long as there are canonical LaTeX
> >> macros for that and
> >> some code points in the Unicode charts that many be (ab)used for our
> >> application.
> >>
> >> Recent examples of Unicode ab-use in Isabelle symbol interpretation are:
> >>
> >> ⤏
> >> ⇢
> >> ⤜
> >> ⪢
> >>
> >> These need to be viewed in Isabelle/jEdit to see the point: the
> >> official shape of the
> >> glyph serves as crude approximation for the intended meaning in Isabelle.
> >>
> >>
> >>  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


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

Re: [isabelle-dev] Multiset insert

2016-07-28 Thread Peter Lammich

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 classes, i.e., occupying the name
plus_multiset.

--
  Peter


> 
> Lovely!
> 
> Jasmin
> 
> ___
> 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] not-exists problem

2016-09-14 Thread Peter Lammich

On Di, 2016-09-13 at 23:35 +, michael.norr...@data61.csiro.au
wrote:
> Note that ∃!x. ∃!y. P x y is not equivalent to ∃!xy. P (fst xy) (snd
> xy).
> 
> If you were going to support ∃!x y at all (and I can certainly see
> the argument for forbidding it outright), I'd expect it to map to the
> first formula above, and not the second.

So there seems to be no consensus on the meaning of "∃!x y".

Btw: I would strongly argue that a proposition like 
"∃!x y. x = abs (y::int)" is wrong, however it holds with the "∃!x.
∃!y"-semantics.

--
  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 have expected:
> > (∄x y. P x y) ⟷ ¬(∃x y. P x y)
> > and
> > (∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))
> 
> +1
> 
> Best,
> Tjark
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/is
> abelle-dev
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[isabelle-dev] Code Folding and errors

2016-09-13 Thread Peter Lammich

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 precise clicking to actually unfold the
content with the error: If the theory is large, it may even be
impossible. 

This is particular annoying when changing existing theories: One wants
to use folding to get a better overview of the theory, and, at the same
time, must be able to quickly locate errors introduced by one's
changes.


Proposal: Display the red exclamation mark icon on the folded line, if
there is an error in the folded content.

--
  Peter

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

Re: [isabelle-dev] not-exists problem

2016-09-13 Thread Peter Lammich

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 funny semantics when used with multiple
variables:

lemma "(∄x y. P x y) ⟷ ¬(∃x. ¬(∃y. P x y))"
by (rule refl)

lemma "(∃!x y. P x y) ⟷ (∃!x. (∃!y. P x y))"
by (rule refl)

this leads to funny lemmas like:

lemma not_what_you_might_think: "∄x y. x+y = (3::int)"
  by presburger

lemma also_strange: "∃!x y. x = abs (y::int)"
  by (metis (no_types, hide_lams) abs_0_eq abs_minus_cancel
equal_neg_zero)


I would have expected:
(∄x y. P x y) ⟷ ¬(∃x y. P x y)
and
(∃!x y. P x y) ⟷ (∃!xy. P (fst x) (snd x))



We should either forbid multiple variables on those quantifiers, or try
to figure out whether there is a widely-accepted consensus on their
meaning.

--
  Peter


> 
> Note that ∄x y. P x y would be fine.
> 
> Larry
> 
> ~/isabelle/Repos/src/HOL: hg id
> dca6fabd8060 tip
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-03 Thread 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 tracking to avoid exactly those
situations, making the kernel robust against data races on the user-
level/in the tools. Is such a tracking possible, how hard would it be
to implement, and how much would it impact performance? I thought about
using level-1 proof terms to track theorem dependencies, and ensure
that they are non-circular, perhaps by simply numbering them in order
of occurrence. Would this be enough?

2. Is there any simple coding policy that guarantees absence of such
problems? Would be: "Do not store cterm/thm + everything containing it
in references" enough, or perhaps: "Do not use Unsynchronized.ref at
all"? (There are lots of usages of Unsynchronized.ref in the Isabelle 
Tools).

-- 
  Peter

-


theory Scratch
imports Main
begin

ML ‹
  val thm = Unsynchronized.ref @{thm TrueI};

  fun sleep 0 = ()
| sleep n = sleep (n-1)

  val _ = thm := (Goal.prove_future @{context} [] [] @{prop "False"}
(fn {context,...} 
=> ALLGOALS (sleep 1000; resolve_tac context [!thm])))
›

lemma F: False
  by (tactic ‹resolve_tac @{context} [!thm] 1›)

end



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

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

2016-12-04 Thread Peter Lammich

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 <makar...@sketis.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 > (isabelle build). > It just uses a prove_future, and proves the theorem with itself!The behaviour is the same in Isabelle2014 and Isabelle2013, whichconforms to my intuition about this aspect of the system. It also meansit is not a regression, so not relevant for the Isabelle2016-1 release.I can't say on the spot what is going on, and if there is a genuineerror somewhere, but I can imagine a conflict of the existing dependencycheck of proof promises with PThm boxes of proof terms.In general, the thm type in Isabelle is definitely not what is beingtold in the common story about the "LCF approach", there is also not"the kernel" in Isabelle. We need to stop telling these tales.Did you encounter this situation in an actual application, or is it anartificially constructed counter-example? That makes an importantdifference, because it is theoretically obvious that Isabelle is not100% correct (just like Coq, HOL-Light, ...).	Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-05 Thread Peter Lammich

Poking on the problem a bit more, I realized that, in the
Isabelle/jedit IDE, promises seem to be never checked. The following
theory works fine in the IDE, but, fortunately, fails in build mode.

I would have expected, at least at some point, to be notified of the
problem (mismatch of promised and proved thm) by the IDE. However, I
can even import Scratch.thy from some other theory, without ever seeing
any error in the IDE. 

--
  Peter


theory Scratch
imports Main
begin


ML ‹
  val thm_f = Future.fork (fn () => @{thm TrueI})
  val thm = Thm.future thm_f @{cprop False}
›

lemma F: False
  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 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 "~~/src/HOL", and some more in the AFP (many of which appear
> > > > to
> > > > be in
> > > > generated code).
> > > So what is wrong here?
> > I find it a bit scary that my first(!) naive attempt to trick
> > Isabelle
> > in presence of multithreading worked out immediately. I do not
> > think
> > that it is a desirable state that Isabelle's soundness depends on
> > correct use of multithreading by the user/tools, and, at the same
> > time,
> > tools are using more and more multithreading. 
> There might be something wrong at the very bottom (which I still need
> to
> figure out later), but your kind of Isabelle/ML code would expose so
> many other problems in practice that is unlikely to lead to a working
> tool.
> 
> This also explains why existing tools have never tripped this odd
> case,
> because they use Isabelle/ML in a canonical (value-oriented) manner.
> 
> 
> > 
> > Btw: I do not believe that the error that I found depends on a
> > (low-
> > level) datarace, it should (not yet tried) also work out if using
> > proper synchronization to make the tactic wait for the theorem.
> It is about circularity. When implementing the parallel proof
> engine  in
> 2007/2008, I was aware that:
> 
>   (1) in practice, circularity hardly ever happens,
> 
>   (2) in theory, it might be a vector for attack.
> 
> So I added some complexity in the implementation to address that, but
> that is still an unfinished area -- there are other conflicts with
> proof
> terms in need of renovation.
> 
> 
> Generically, Isabelle as a system is relatively hard to grasp. It is
> surprising that it works so well, such that empirically most users
> think
> that it is unbreakable.
> 
> This is mainly a social problem, and needs to be solved there.
> 
> 
>   Makarius
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-01 Thread Peter Lammich

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 ???
> 
> 
> 
> Thanks,
> 
> David Blubaugh
> Electrical Engineer
> ATR Associate
> 
> 
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2017-08-16 Thread Peter Lammich

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: Makarius To: Tobias Nipkow ,isabelle-dev@mailbroy.informatik.tu-muenchen.deCC: On 16/08/17 16:10, Tobias Nipkow wrote:> > Concerning "sorted_by" vs "sorted_wrt": the latter seems closer to> informal usage. But if many people cry out for "by" we could change that.In Isabelle/ML we used to have "sort_wrt" for some decades, but I havechanged that recently into into "sort_by" to make it coincide with theterminology of the Scala library.Seehttp://isabelle.in.tum.de/repos/isabelle/rev/610794dff23c	Makarius___isabelle-dev mailing listisabelle-...@in.tum.dehttps://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] PolyML update

2017-08-11 Thread Peter Lammich

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_Word. In doing so, I realised that PolyML in 64 bit mode has a bug in the Word64 implementation in the version that the current development version 2a6371fb31f0 uses (PolyML 5.6-1). For example, dividing 18446744073709551611 by 3 using the Word64 structure gives a wrong result. The problem seems to be fixed in PolyML 5.7. I am now hesitant to update my AFP entry because (1) I cannot include all the test cases for Uint64 that I want and (2) if PolyML 5.6-1 is also shipped with the next release, then users might prove False by exploiting this error.Are there any plans to update to PolyML 5.7 before the release?Andreas___isabelle-dev mailing listisabelle-...@in.tum.dehttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2018-01-16 Thread Peter Lammich

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
> 

> > 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> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2018-03-06 Thread Peter Lammich

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/transfer), you have to type "(=)" frequently.


Is it possible to keep (= bound to \, but exclude it from
immediate completion?

--
  Peter



On Mi, 2018-01-10 at 20:17 +0100, Tobias Nipkow wrote:
> * The "op " syntax for infix operators has been replaced by
> "()". If  begins or ends with a "*", there needs
> to
> be a space between the "*" and the corresponding parenthesis.
> INCOMPATIBILITY.
> There is an Isabelle tool "update_op" that converts theory and ML
> files
> to the new syntax. Because it is based on regular expression
> matching,
> the result may need a bit of manual postprocessing. Invoking
> "isabelle
> update_op" converts all files in the current directory (recursively).
> In case you want to exclude conversion of ML files (because the tool
> frequently also converts ML's "op" syntax), use option "-m".
> 
> In revision eab6ce8368fa
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
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?

2018-11-08 Thread Peter Lammich

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 syntax!Peter Original Message Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?From: Makarius To: isabelle-dev CC: Over the decades we have accumulated funny quotation forms in Isabellesyntax that are often hard to explain to new users (also to old users).In particular, what are the remaining uses of {* ... *}?It should already be superseded by cartouches. There is also "isabelleupdate_cartouches" to get rid of it (as well as `alt_string`).The long-term trend is to converge to cartouches or double-quotes almosteverywhere. Cartouches are for nested languages, and double quotes forstring literals or names that are in conflict with other syntax.	Makarius___isabelle-dev mailing listisabelle-...@in.tum.dehttps://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] syntax highlighting of inner comments

2019-03-06 Thread Peter Lammich

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, but having highlighting at least.Peter Original Message Subject: [isabelle-dev] syntax highlighting of inner commentsFrom: Fabian Immler To: isabelle-dev@mailbroy.informatik.tu-muenchen.deCC: Hi,Up until Isabelle2018, I used (* ... *) to comment out parts of lemmas/definitions, mostly for debugging larger expressions.Highlighted in red, (* ... *) was nicely set apart from the rest of the _expression_.Now (e.g., isabelle/b58a575d211e) we can use \<^cancel>, but its "highlighting" in black makes it very hard to keep an overview.Note that e.g., with a type error in a lemma statement, canceled text is highlighted red (like in the attached screenshot).Best regards,Fabian___isabelle-dev mailing listisabelle-...@in.tum.dehttps://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 DejaVu against old Isabelle Text font

2019-02-10 Thread Peter Lammich

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
> (Fedora 29 with i3) setup. Thanks!
> 
> chris
> 
> On 2/10/19 7:47 PM, Makarius wrote:
> > 
> > On 08/02/2019 10:03, Christian Sternagel wrote:
> > > 
> > > 
> > > I am glad to hear that others have the same experience, I thought
> > > my
> > > eyes were going bad ;)
> > > 
> > > But seriously, "buy a new screen" is not always possible. For
> > > example,
> > > in the upcoming summer term I am teaching an Isabelle class at
> > > the
> > > University of Innsbruck. In my experience (and I just reconfirmed
> > > this
> > > for the room I will be teaching in), the projectors we have here
> > > a
> > > typically rather old (and have low resolution, but that is a
> > > different
> > > story).
> > > 
> > > At the moment there is a palpable difference (font rendering
> > > crispness
> > > wise) between using Isabelle2018 with projector (which I will do
> > > anyway
> > > for my class) and some recent development version (sorry I didn't
> > > note
> > > down what changeset I used for testing my setup).
> > Classic JDK 8 from Oracle and OpenJDK 11 (e.g. from AdoptOpenJDK)
> > are
> > different in many ways, and it is definitely required to get used
> > to the
> > new look of font rendering. (For me Isabelle2018 already looks very
> > strange.)
> > 
> > With proper parameters -- in software and hardware -- fonts should
> > come
> > out better than before.
> > 
> > 
> > First of all, sub-pixel rendering should be enabled, see this NEWS
> > entry
> > from Isabelle/f714114b0571 (25-Oct-2018):
> > 
> >   *** Isabelle/jEdit Prover IDE ***
> > 
> >   * Improved sub-pixel font rendering (especially on Linux), thanks
> > to
> > OpenJDK 11.
> > 
> > (In Java 8, sub-pixel rendering made things worse.)
> > 
> > Since that that NEWS entry is a bit too implicit, I have now
> > changed the
> > default to enable "Subpixel HRGB" always on all platforms
> > (Isabelle/f610115ca3d0). I have checked my usual test machines for
> > Windows and macOS, to see that it all looks fine.
> > 
> > 
> > Secondly, I have done some more research on FreeType, the renderer
> > used
> > for OpenJDK on Linux. It appears that the DejaVu family gets some
> > special treatment if it shows up under its original name, but not
> > if it
> > is a renamed copy. So I have fine-tuned the Isabelle DejaVu fonts
> > in
> > Isabelle/4791988fcbc4 to impose the FreeType auto-hinting
> > beforehand to
> > the TrueType file: this leads to isabelle_fonts-20190210 in
> > Isabelle/7e5a7a11d5d1.
> > 
> > 
> > In summary:
> > 
> >   * Isabelle font rendering should be once again slightly better on
> > Linux.
> > 
> >   * There is a small risk that it has slightly degraded on Windows
> > and
> > macOS.
> > 
> > In other words: early adopters should look closely if it is all
> > fine. We
> > are (very slowly) moving towards the Isabelle2019 release
> > (presumably
> > June 2019), and everything needs to be beyond doubt when released.
> > 
> > 
> > Makarius
> > 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabel
> le-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2019-02-01 Thread Peter Lammich

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. Because gratchk is also bundled with
gratgen, which is implemented in C++, I have not yet put it into the
AFP, b/c that would mean to separate gratchk from gratgen, or to push
C++ code to the AFP, for which I cannot expect an build infrastructure
there.

2. In the AFP, there is the CAVA model checker. It also comes with some
external ML code. I just checked, and this external ML code is already
severely bit-rotten, as it has not been maintained for years now ... at
latest the recent string-literal reform should have reliably killed it.
 
Also, timing regression tests are important when doing such reforms as
the above-mentioned string-literal reform, which has the potential to
severely slowdown the generated code.

--
  Peter



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

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

2019-01-31 Thread Peter Lammich

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: file-system covers that already, i.e. we should
> be
> able to eliminate almost all generated files from the AFP repository.
> 
> So "export_code .. file" should just disappear -- it is semantically
> illtyped in PIDE: editing the "file" argument will leave a trace of
> machine oil spilled to the physical file-system.

The problem here is actually deeper: 
Many AFP-entries are designed to export code which then works together
with some external code. However, there seems to be no way to test
whether this external code works with the generated code. 

There is the "checking"-option, which will test the generated code in
isolation. But any external code that is supposed to interface with the
generated code is left to bit-rotting.

--
  Peter

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

71 matches

Mail list logo