Hi Clemens,
I hope,
though, it has become clear that I'm not opposed to having
interpretation in locale contexts by principle, I'm merely opposed to
explaining them in the way you propose.
I still see us disagree on how far the local theory game can be driven
wrt. interpretation,
There is a record of a rough talk I gave recently concerning Big
Operators. It might be of interest for a wider audience.
Please note that it is really rough, with the audience sometimes
assisting me to present things the most comfortable way nowadays in
jedit ;-).
The record of the
Hi Clemens,
Let those thoughts sink further few days. If there is no veto until
Apr
7th, I would go ahead to turn the patches upstream.
You have proposed a change about which doubts were raised. I don't
consider it acceptable to then announce a deadline after which you will
go ahead and
context B begin
context
begin
interpretation A
end
end
This looks attractive, but could you please elaborate the semantics:
- What would be the effect of the interpretation from the inner block on
the outer block?
The interpretation would only affect the inner block.
- What
By accident, this is now Min.subsumption. I will revert this to
Min.in_idem ASAP.
See now #7c59fe17f495.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital
Before this revision there we had the lemma Min.in_idem. What replaces
this lemma?
By accident, this is now Min.subsumption. I will revert this to
Min.in_idem ASAP.
The Big Operators material had became so entangled over the years (me
being not guiltless in that respect) that in large parts I
Hi Manuel,
I just noticed that when exporting code to Haskell, there is a
complication when some of the theories involved have lower-case names.
The code export itself will work with no error or warning, but when
ghc/ghci are invoked on the generated code, they will report the
lower-case
Right now we should merely have clear terminology in the discussion.
The language keywords can be finalized later.
Indeed. In this delicate corner, modifying surface syntax makes little
headache. Lets get right the mental model and the internal
implementation first.
Note that 'interpret'
context B begin
interpretation A
interpretation A'
interpretation A''
end
sublocale B A''
What you currently have in many places (e.g.
http://isabelle.in.tum.de/reports/Isabelle/file/757fa47af981/src/HOL/Lattices.thy)
is the pattern.
context B begin
…
end
sublocale B …
You might still argue about syntax, e.g. having separate commands
subscription – what is currently interpretation and subscription, not
in free-floating contexts (as implemented in the patches).
interpretation – only in confined contexts (locales, context begin …
end, but not global
After one further round of thinking, I would still suggest
* »interpretation« for interpretation without subscription
* »subscription« for interpretation with subscription
I think it is worth to distinguish these on the surface. Maybe future
will bring different possibilities with »private« or
Semantically, do you remember reasons why we did not consider it so far,
or was it just forgotton or lost in state-budget problems? We have a
little bit of budget now after the release and towards the summer, but
we need to stay within a reasonable range of complexity.
Well, we always have
Hi Clemens,
nice to hear from you.
Let me add my perspective here, and see how we can converge.
2. sublocale and interpretation are more different than it looks:
interpretation provides inheritance of mixins (or, from the user
perspective, rewrite morphisms) and it is possible to amend
There is a series of minimal invasive patches to generalize
»interpretation« / »sublocale« to »interpretation« in arbitrary targets,
not just theories and locales. The patches are inspectible at
http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation
Explanations follow. It is
cf. doc/maintenance.html:
Check out the archive from the mercurial repository with:
hg clone ssh://login@afp.hg.sourceforge.net/hgroot/afp/afp afp-devel
But
hg pull ssh://fhaftm...@afp.hg.sourceforge.net/hgroot/afp/afp
yields
Remote: abort: There is no Mercurial repository here (.hg not
Am 23.03.2013 14:05, schrieb René Thiemann:
Dear all,
I recently got some message from sourceforge, that they changed their
directory structure. So I have no problems accessing the afp at
ssh://login@hg.code.sf.net/p/afp/code
Thanks a lot. With an updated AFP I now see that the
* Revised devices for recursive definitions over finite sets:
- Only one fundamental fold combinator on finite set remains:
Finite_Set.fold :: ('a = 'b = 'b) = 'b = 'a set = 'b
This is now identity on infinite sets.
- Locales (»mini packages«) for fundamental definitions with
Hi Alex,
What is the current (as of, say, d5c95b55f849) method for getting
exception traces? I am trying to debug a low-level exception such as
exception Match raised (line 287 of term.ML)
which happens somewhere below partial_function. Some years ago there
used to be Toplevel.debug
In private conversation, there has been some confusion concerning this
issue (stemming from the users mailinglist originally).
Let me clarify, quoting the tutorial on code generation:
--
Code_Binary_Nat implements type nat using a binary rather than a linear
representation, which yields a
* Numeric types mapped by default to target language numerals:
natural (replaces former code_numeral) and integer (replaces
former code_int). Conversions are available as integer_of_natural /
natural_of_integer / integer_of_nat / nat_of_integer (in HOL) and
Code_Numeral.integer_of_natural /
Isabelle/0a55ac5bdd92 is the merge point for the release branch from
https://bitbucket.org/isabelle_project/isabelle-release
Now the main Isabelle repository is again the main focus for working
towards the next release.
what is the policy for AFP then at the moment? Are changes which go
Experts on HOL's structure are welcome to reconsider it eventually. For
the release we should not open that can, though.
See now http://isabelle.in.tum.de/repos/isabelle/rev/da97167e03f7.
There is no observable effect on runtime behaviour:
on lxbroy10 with Plain.thy
Running HOL ...
Hi Gerwin,
Isabelle/0a55ac5bdd92 is the merge point for the release branch from
https://bitbucket.org/isabelle_project/isabelle-release
Now the main Isabelle repository is again the main focus for working
towards the next release.
what is the policy for AFP then at the moment? Are changes
Hi Alessandro,
Is there any plan to make things in the library more uniform (one way or
the other)? Is there a preference for new type classes should be
developed (purely syntactic or with assumptions)?
well, there is no big masterplan. Usually things evolve: somebody
thinks about an
Maybe there is some confusion what the semantics of hide (open) is
exactly supposed to be. But since the current state of affairs gives
no tool at hand to resolve situations as sketched above, this is a
serious obstacle.
The hide feature was added as a temporary workaround for the lack of
Am 07.01.2013 13:06, schrieb Makarius:
This is a left-over from the isabelle build reform from last summer: Do
the additional HOL images still have a purpose? Notably:
HOL-Base
HOL-Plain
HOL-Main
If it is just for experimentation, these session can be easily provided
by 1 line
This is a left-over from the isabelle build reform from last summer: Do
the additional HOL images still have a purpose? Notably:
HOL-Base
HOL-Plain
HOL-Main
If HOL-Plain vanished, the same could apply to Plain.thy itself.
Florian
--
PGP available:
Here something seems indeed to be wrong with the class edge completion
in axclass.ML. I have attached a more minimal example and will
investigate further.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
The graphview plugin, despite significant progress in the past weeks
esp. wrt. performance, is IMHO still not suitable to manage our typical
graphs (in particular class_deps), mainly due to too small-sized nodes
resp. too wide distances. Unfortunately, the print mode
So far. I will stop for today, and I am not sure when I am able to turn
back on the issue. But maybe I have found enough that the original
authors can comment on it.
Yet an even more minimal example
Cheers,
Florian
--
PGP available:
We are officially still on stable scala-2.9.2, but the Scala guys are
moving slowly towards scala-2.10.0, so it is worth testing that aready.
I've got the subject wrong: the tested version is scala-2.10.0-RC2.
See now http://isabelle.in.tum.de/reports/Isabelle/rev/e21485358c56 etc.
Hi all,
I have the situation that I want to define via primrec a function with
an existing popular name (append) but retain the commonplace accesses
append for List.append and append.simps for List.append.simps (see
attached theory for a contrieved example). With the existing semantics
of hide
I have the situation that I want to define via primrec a function with
an existing popular name (append) but retain the commonplace accesses
append for List.append and append.simps for List.append.simps (see
attached theory for a contrieved example). With the existing semantics
of hide
Thanks a lot for that thorough analysis!
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
Hi Alessandro,
On a semi-related topic, I was wondering why the Isabelle library has
syntactic type classes for many (most?) operators but not for bot and top.
this is mainly a result of historic developments and compromises.
Especially the long-standing operators plus, times etc. have been
Hi all,
I would like to add that there is also the config_tum repository, which
Florian created when he wanted administrative information neither in the
Wiki nor in the public Isabelle repository. I probably would have looked
there (as it contains some mira administration info), but never
Hi all,
The reason is that Open_Induction/ROOT (and also
Open_Induction/Open_Induction.thy) relies on $AFP being set, which is
only the case if AFP is registered as a component (which is not the case
for Mira).
I would recommend that mira incorporates AFP as component, since this is
what we
The new isabelle build tool is really a joy to work with -- thanks
Makarius! :-) But one of the mistakes I find myself doing over and over is
typing
isabelle build HOL
when I really meant
isabelle build -b HOL
me too ;-)
Florian
--
PGP available:
Am 03.12.2012 14:24, schrieb Johannes Hölzl:
Fabian and I found the missing check in Cooper's algorithm
(src/HOL/Tools/Qelim). The fix can be found in the testboard
52e97a5f5e25. If it works I will push it to the Isabelle repository.
- Johannes
Thnx a lot!
Florian
--
PGP
The latter aspect is gradually being superseded by the ROOT setup: it
tells which collection of theories (without merging) contribute to a
session. In the next round of the reforms the Prover IDE should be able
to import all of them in interactive mode, like build does in batch mode.
I'm
Am 21.11.2012 14:29, schrieb Makarius:
On Wed, 21 Nov 2012, Makarius wrote:
We are officially still on stable scala-2.9.2, but the Scala guys are
moving slowly towards scala-2.10.0, so it is worth testing that aready.
I've got the subject wrong: the tested version is scala-2.10.0-RC2.
Anybody any ideas what went wrong!?
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
Bijection then produced this:
The first bad revision is:
changeset: 49948:744934b818c7
user:haftmann
date:Sat Oct 20 09:12:16 2012 +0200
summary: moved quite generic material from theory Enum to more
appropriate places
I can't say for sure if this is a correct
I first thought it would be related to 1167c1157a5b (haftmann on
src/Pure/Proof/extraction.ML), which is not immediately easy to follow
in every detail.
It indeed isn't, but the effect is idempotent.
To my defence, reordering arguments is not very comprehensible from a diff.
Florian
In such cases, the general question is if making the sources canonical
has any purpose. It is rather old material by Stefan Berghofer, written
in the typical style from around 2000, and not going to be revisited in
the foreseeable future.
It is, as part of the story Spec_Rules vs. code
Hi Ondrej,
But your observation gave me an idea that actually I should remove the
explicit names for morphisms in Mapping.thy completely and then you
wouldn't even notice there are any abstraction and representation
functions behind the scene.
I would conclude that if abs and rep are
Does anybody remember a use of the 'apply_end' command?
Yes, there are two in JinjaThreads (theory J/ProgressThreaded), although
they could be fused into the qed. However, I regularly use apply_end
when I develop the method call for qed to finish off all the remaining
cases after having dealt
Here are the names I would prefer:
mult_add_left: (a + b) * c = a * c + b * c
mult_add_right: a * (b + c) = a * b + a * c
The above names follow the pattern of many rewrite rules already in
the Isabelle libraries:
Convincing argument.
Florian
--
PGP available:
Hi Lukas,
in the changeset e8400e31528a of the Isabelle repository, you moved the
theorem Pair_inject in the Product_Type theory into a section called
Legacy theorem bindings and duplicates.
In my current development, I rely on the theorem Pair_inject, and it is
the most suitable rule for
Hi all,
the recently established graphview IMHO has currently two disadvantages:
* Misfit of node annotation size wrt. to the size of the full graphs –
node annotations are not readable within a reasonable size coverage of
the graph.
* Does not scale well (e.g. class_deps from Main.thy).
What
The class_deps non-scalability probably stems from the omission of the
transitive reduction (Hasse diagram). This was probably done due to the
anticipated locale graph visualization (which does not quite work), or
it might be just an omission.
The latter. I am not aware of any locale graph
I cannot connect to testboard at the moment, it seems to be in bad
shape again.
The testboard should now be in a running state again.
For the record: is there any diagnosis what went wrong?
Florian
--
PGP available:
Hi Ondrej,
I stumbled over
http://isabelle.in.tum.de/repos/isabelle/rev/558e4e77ce69
where you have introduced Finite_Set.fold which on finite sets is equal
to Set.project (cf.
http://isabelle.in.tum.de/repos/isabelle/rev/558e4e77ce69#l1.41) and on
infinite sets is underspecified.
Would there
Hi all,
I stumbled over some comments »(* FIXME: move to Set theory *)« in
Finite_Set.thy.
Note that with jEdit it is now really easy to edit the HOL theories
interactively:
isabelle build -b Pure isabelle jedit -l Pure thy files
So, you can get your intention done directly and need
Florian also has an older attempt at some testafp tool in the AFP
repository, which should be obsolete now.
This is obsolete now. Anyone still having stocks there?
Florian
--
PGP available:
Hi again!
On our running gag list with have at least these related issues:
* codgeneration as sketched above
* behaviour of the Simplifier on seemingly atomic constants c (due
to abbreviations) that are actually of the form loc.c x y z
* stability and expectedness of
The current infrastructure has only a preprocessor applied *after* the
internal bookkeeping (for reasons I will explain in a separate, long
promised mail), so this would add further complexity here.
What sets the code generator apart from other tools is that theorems are
never stand-alone but
Currently, we have still the ancient walking-by of doc sessions (e.g.
IsarImplementation – note the CaMeL case) and corresponding document
names (e.g. implementation). Is there anything speaking against
unifying these now?
Florian
--
PGP available:
* to adjust the technical conditions accordingly. A single critical
point is the »administrative repository« access at TUM, about which
certain ideas have been floating around over the last years but which
never evolved into technical consequences, e.g.
* moving the »main« repository from
Hi Lars,
Most space seems to spend with Isabelle_makeall and AFP runs, amounting
to 4-5GiB each. Has someone an idea what changed?
If yes: do we want to revert to store less stuff again or should we
implement some kind of automatic cleanup?
can you provide us with a du dump or something
Dear all,
I am in a similar situation as Alex since I will leave tomorrow morning
for a one-week-trip (offline!), so I can just spend my few cents here.
Tjark, you have no business here.
This is, finally, too much for me!
I trust that the community as a whole will come to the conclusion
(want to add something for clarity)
* to adjust the technical conditions accordingly. A single critical
point is the »administrative repository« access at TUM, about which
certain ideas have been floating around over the last years but which
never evolved into technical consequences, e.g.
For the record:
I did not know that Tjark had conversed with Florian privately before.
This removes the main accusation on his
http://isabelle.in.tum.de/repos/isabelle/rev/2db8aa3459d4 where it was
looking like he was seizing control of the draft started by Florian.
The email reads (in
Hi Clemens,
clemens-ballarins-macbook-air:IsarRef ballarin$ hg push
Password:
remote: Not trusting file
/home/isabelle-repository/repos/isabelle/.hg/hgrc from untrusted user
wenzelm, group isabelle
pushing to
Hi Alex,
Today, I've completed the (long overdue) migration of the mira database
from Florian's old machine to a proper server (hosted on
isabelle.in.tum.de).
thanks a lot, this is the successful accomplishment of one of our
long-running IT projects…
I assume, if I don't get a rollback until
Anyway, I've lost a bit track of the lastest bash movements. It is more
and more being replaced by Scala anyway. (Maybe one should make a
precise getopt imitation in Scala, with all the official features of
-abc ARG option conglomerates and -- etc.).
Maybe this is a source of inspiration:
I wonder whether there is a possibility to generalize the session
concept to other generates beyond tex as well, in particular generated
code, e.g.
session Foo = HOL +
theories
…
theories
Bar [export_code = blubb in SML]
…
This would subsume the rather arcane »isabelle codegen«,
*** System ***
* Advanced support for Isabelle sessions and build management, see
system manual for the chapter of that name, especially the isabelle
build tool and its examples. Eventual INCOMPATIBILITY, as isabelle
usedir / make / makeall are rendered obsolete.
Two things come to my
cf. http://isabelle.in.tum.de/reports/Isabelle/rev/ffa0618cc4d4:
* Library/Debug.thy and Library/Parallel.thy: debugging and parallel
execution for code generated towards Isabelle/ML.
Florian
--
PGP available:
text {*
FIXME -- Evaluation with @{text Quickcheck_Narrowing} does not work, as
@{text code_module} is very aggressive leading to bad Haskell code.
Therefore, we simply deactivate the narrowing-based quickcheck from here on.
*}
I do not unserstand this. What does code_module mean
Hi Clemens, hi Makarius,
let me resume this running thread (not necessarily gag).
Let me quote two emails by Clemens on this issue:
What is called mixin in the implementation is a transfer principle that is
applied in addition to the interpretation morphism. Currently users can only
give
Hi Clemens, hi Makarius,
let me continue concerning syntax:
The current syntax in Tools/interpretation_with_defs.ML is just a proof
of concept:
interpretation L inst
where
bar = t
defines f is foo
A much better idea could be to give the new defs in a for-clause:
interpretation L inst
Hi all,
cs. http://isabelle.in.tum.de/repos/isabelle/rev/3a5a5a992519 was an
attempt to make results of `export_code` with relative file path more
predictable. There my assumption was that Thy_Load.master_directory
would point to an absolute path, particulary the location of the current
theory,
Hi all,
tomorrow Wed10th in the morning (GMT) there will be an interrupt in the
testboard due to maintainance works on the macbroy15 machine hosting its
database.
Sorry for any inconvenience,
Florian
--
PGP available:
Hi all,
tomorrow Wed 11th in the morning (GMT) there will be an interrupt in the
testboard due to maintainance works on the macbroy15 machine hosting its
database.
(Wed 11th of course, *not* 10th)
Sorry for any inconvenience,
Florian
--
PGP available:
I have consolidated the story further:
* central hook Admin/init_components does not use platform-specific
component files any longer but relies on good old universal components
* mira uses this hook (after the next crash of the daemon and the
following implicit restart)
@Gerwin: maybe you
It means ProofGeneral-4.1 will be there by default, if Florian's way to
init the components for repository versions is used. So after
sufficiently many people have picked up that scheme, the old guess mode
via choosefrom can be discontinued.
See
* Will the idea of platform-universal components revived? If yes, the
platform-sensitive components files can be discontinued. I personally
like the idea, though?
The problem is that modern operating systems suffer from a
multi-personality problem. There is not the platform that you are
running
Tiny instructions on changesets c97656ff4154 ff.:
* include the following snippet into your ~/.isabelle/etc/settings:
source ${ISABELLE_HOME}/Admin/init_components
* obtain components from Isabelle2012, http://isabelle.in.tum.de/dist or
nfsbroy:/home/isabelle/contrib; hints which components
@Florian: so your suggestion would be that there are several components
files in Admin, say Admin/contributed_components_x86-linux containing
contrib/x86-linux/jdx-6u31-x86_linux
contrib/e-1.5
...
Then the extra path component is redundant, and I think I would rather
go without
PS: I am just playing around with a locale for finite trees and wanted
to introduce some recursive functions (and later also inductive
predicates) but pattern matching is only possible on constructors. Is
anybody aware of an earlier attempt for doing such a thing or a better
way to prove
Hi all!
The following is for my own home directory at TUM:
.isabelle/etc/components -
/home/wenzelm/isabelle/repos/Admin/contributed_components
.isabelle/contrib - /home/isabelle/contrib
This achieves the effect of versioned symlinks: the repository says
which directories to take
I first intended to do the same as for Isabelle2011-1, but then realized
that Isabelle2012 had diverged further from the old universal scheme
of add-on packages: more and more components are specific for one of the
platform families (linux, darwin, cygwin), and would have required some
extra
Hi all,
for years now, there was a silent convention that
~isabelle/contrib_devel at the TUM NFS would contain references to
more-or-less up-to-date add-on components for Isabelle. Is there
currently anybody still doing maintainance there? Also, the local
Isabelle2012 distribution in
Hi again,
/home/isabelle/contrib_devel/jdk-6u31_x86_64-linux
/home/isabelle/contrib_devel/jdk-6u31_x86-linux
This seems to indicate that the JDK component does not follow the common
COMPONENT/PLATFORM/… scheme for components. Is there any reason for this?
Florian
--
PGP available:
Hi Bertram,
just a curious question: in which context are you using the Isabelle
code generator?
CU,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
Hi all,
just a synopsis of the whole matter of sort constraints for constants.
a) Sort constraints for code generation. Concerning sort constraints
and datatype constructors, everything has been said already in this
thread. Generally, for code generation sort constraints *have*
operational
Hi all,
In the short term, we could move the FinFun theory into the HOL library
of the development version after Isabelle 2012 and the AFP 2012 has been
released, if we agree that this moves this contribution in the right
direction.
some remarks on my behalf:
a) Ideally, tools
Hi Christian,
I spotted this strange line in the NEWS (linked from the test website)
symp_def ~ (dropped, use symp_def and sym_def instead)
the LHS is before, the RHS is after the change. In particular, the
symp_def from the RHS is another one than that form the LHS.
Hope this helps,
It is confusing/wrong to say that symp_def was dropped when we still
have a theorem by that name.
Perhaps the line should read something like this:
symp_def ~ (modified, use new symp_def and sym_def instead)
Done.
Florian
--
PGP available:
Hi Christian,
recently I reinvented (a tiny) wheel. In my well-quasi-order AFP entry I
use suffixes of lists (mainly to do induction over suffixes, but
anyway). Afterwards (by chance) I found Library/List_Prefix which
defines the same thing under the name postfix.
Moreover I used another
I've managed to remove more than 5 GB of old heap files, but this might
be a bit pathethic due to this directory:
225G tmp/shared_results
Does anybody know what it is?
These are the results from the mira runs, which in theory are kept
eternally. There is the mira command »purge« which
I also set sidekick.complete-delay=0, so I can just keep typing, as I
did in emacs.
For me \t does not work as an accept character (nothing happens when I
type \t... that's the only reason why I use \n). Also, when setting
the delay to 0, I sometimes (nondeterministically it seems) end up in
Hi Alex,
while backporting HOL/Library/Set_Algebras to use type classes again (a
remaining point of the 'a set transition),
thanks for doing this!
I noticed that there is now a
clone of that file in HOL/ex.
What should we do with the clone? Are there maybe other examples that
can
Hi all,
The overloading rules are quite tricky. I don't understand why the first
instantiation requires a definition of sup_hf (including the type in the
constant name), while the second one simply requires a definition of minus.
Perhaps because there is an explicit type in the first
Hi all,
- I would like to add a size limit to records beyond which no code generator
setup is performed. The main reason is that on sizes 200 fields or so, the
setup does not make any sense, but consumes very large amounts of memory (and
time). Switching it off gets rid of almost all of
Does anybody have experience with the more recent hg rebase? An early
version of it 3 years ago was causing problems, but one can probably
expect this to be ironed out now.
I nowadays use »hg rebase« regularly, most times with the idiom »hg pull
--rebase«, and it seems to serve its purpose.
Hi Christian,
it seems as if a recent change (in the repo version; within the last 2
weeks, but I do not know exactly when) fixed the naming of type
variables inside instantiations.
I guess this is a consequence of the recent local theory infrastructure
refinements – whether intentional or
Florian can say, if he originally meant to support different type
variable names as shown above. There might be some type improvement in
the context that needs to be re-adjusted (or some now unused things to
be removed).
The assumption has always been that type variable carry canonical names
Hi Christian,
Sorry, I'm not familiar with the developer workflow. I do have a
cloned hg repo of Isabelle (from
http://isabelle.in.tum.de/repos/isabelle), but I don't see an
IsaMakefile (which would be required for isabelle make all). Where is
this IsaMakefile located?
it is »isabelle makeall
401 - 500 of 672 matches
Mail list logo
