Re: [isabelle-dev] jEdit import theories
I used a literal ~ and changing this to $HOME solved the problem, thanks! cheers chris PS: Is it just me or is Isabelle/jEdit really much faster than ProofGeneral/emacs when loading theories? (Maybe this is due to some other difference between Isabelle2011-1 and the repo version; I only use emacs if I have to stick to Isabelle2011-1.) On 03/21/2012 01:24 AM, Makarius wrote: On Tue, 20 Mar 2012, Christian Sternagel wrote: Hi there, I am using an environment variable in an import statement like imports $VAR/Theory.thy in batch-mode this works fine. However, in jEdit I get an error message indicating Missing theory (file ...) where the path in the error message shows that $VAR was used relative to the path of the surrounding theory file. $VAR contains something like ~/some-path and was intended as being applied globally. changeset: e3a3f161ad70 jedit_build: 20120313 Odd, I think it should work. There is an explicit treatment of symbolic Isabelle paths (with a certain notion of variables) and the jEdit/JVM platform path notion. See also http://isabelle.in.tum.de/repos/isabelle/file/1ab41ea5b1c6/src/Tools/jEdit/src/jedit_thy_load.scala#l22 What does not work right now is to use VFS paths of jEdit together with Isabelle ones. I would love to see theory sources being loaded via ssh or http at some point ... In the example above, do you have a literal ~ or its expansion by the operating system shell? It is more robust to use $HOME in shell scripts if you mean home. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] sets and code generation
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
In the NEWS I found that the default setup for sets during code
generation is as a container type (instead of predicates). What are the
reasons for this decision? Is there an easy fix for such code equations?
One other thing. Syntax (e.g., ord) suggests 'a = 'a = bool for
relations, but the library support (starting with more standard symbols)
is leaning towards 'a rel. As a user it would be nice to have some
indication what is preferable/best practice (e.g., in terms of future
support; I already switched several times in our IsaFoR formalization,
currently rewrite relations are of type ('f, 'v) term rel, is this the
way to go?).
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of op | on the type ...
set. To execute this, you have to move this specification to predicates
('a = bool):
Define op | = (%(x, y). supt_impl x y)
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of op | on the type ...
set. To execute this, you have to move this specification to predicates
('a = bool):
Define op | = (%(x, y). supt_impl x y)
Lukas
Sorry I don't quite get it. op | is already defined to be of type
('f, 'v) term rel (and used heavily as a set). So the above equation
would not be well-typed. Is your suggestion to change op | into a
predicate?
cheers
chris
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
On 03/21/2012 09:08 AM, Christian Sternagel wrote:
On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
Hi there,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
as a code equation leads to an error stating that terms (x and y are
first-order terms) do not support the enum class. Since the possible
terms (using strings as function symbols and variables) cannot be
enumerated in a (finite) list, I can also not introduce an enum
instance.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of op | on the type ...
set. To execute this, you have to move this specification to predicates
('a = bool):
Define op | = (%(x, y). supt_impl x y)
Lukas
Sorry I don't quite get it. op | is already defined to be of type
('f, 'v) term rel (and used heavily as a set). So the above equation
would not be well-typed. Is your suggestion to change op | into a
predicate?
cheers
chris
Yes.
If you have an infinite set during the execution in the generated code,
which you hinted at before, you cannot use the type 'a set for code
generation, but you must use 'a = bool.
I cannot estimate how much work that is in your case.
If it is unfeasible in your formalisation to change this, there might
also be other means to obtain an executable specification by creating an
alternative data refinement for sets, but I only had this in the back of
my mind, and we have not done this (yet).
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit import theories
On Wed, 21 Mar 2012, Christian Sternagel wrote: Is it just me or is Isabelle/jEdit really much faster than ProofGeneral/emacs when loading theories? (Maybe this is due to some other difference between Isabelle2011-1 and the repo version; I only use emacs if I have to stick to Isabelle2011-1.) Ça depend, as the French like to say. Isabelle/jEdit in Isabelle2011-1 and repository versions until today (8e1b14bf0190) uses a uniform model to process buffer content, intermixed with potential user edits, with full document markup reports that eventually causes the Haribo effect in the sources. This is done in a reasonably fast way, but there are still situations where too many goal states are printed and thus the prover session gets overloaded. (E.g. in Hoare_Parallel or AFP/JinjaThreads.) In contrast, Proof General / Emacs is very slow in processing the current buffer (especially on Mac OS), but resolves imports via the batch-mode theory loader of Isabelle, which is presently faster than any other way of processing theories. (The same is used for isabelle usedir/make/makeall.) The general direction is to unify old-style batch loading with new-style document processing, such that it is both very fast and produces the full markup. It will also overcome occasional confusions about different behaviour of tools in different modes of theory processing. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sets and code generation
Hi Christian,
since set is a proper type some code equations that used to work, no
longer do, e.g.,
op | = {(x, y). supt_impl x y}
there is a couple of issues you are hitting at here.
A. The (re-)introduction of the set type constructor
See
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01736.html
for one possible entry into the motivation and discussion concerning that.
B. The default code generation for setup
You can always turn back to sets-as-predicates by
code_datatype Collect
and then proving appropriate theorems for the set operation etc. – this
would fir best into a library theory which could then be part of the
distribution. But I guess your issue is mainly with…
C. Relations
Both kinds of relations 'a = 'a = bool and ('a * 'a) set are present
in their own right, but with disjoint developments in the HOL theoris.
Note that you can convert between both using pred/set conversions, the
same infrastructure as inductive_set is using.
So, if you want predicate relations, it seems to be best to convert your
stuff to them, filling existing gaps in the HOL theories by additional
definitions and suitable pred/set conversion declarations.
See theory Relation for examples for making use of pred/set
conversions by means of attributes to_set and to_pred; and
declarations of pred/set conversions by means of attribute pred_set_conv.
Unfortunately, there is no reference for them in the Isabelle Reference
Manual. Maybe one day this is subsumed by an emerging generic »lifting«
infrastructure.
Hope this helps,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
