[isabelle-dev] NEWS: HOL-Spec_Check -- a Quickcheck tool for Isabelle's ML environment
* HOL-Spec_Check: a Quickcheck tool for Isabelle's ML environment. With HOL-Spec_Check, ML developers can check specifications with the ML function check_property. The specifications must be of the form "ALL x1 ... xn. Prop x1 ... xn". Simple examples are in src/HOL/Spec_Check/Examples.thy. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading
Dear all,
as I said earlier I am trying to make some changes (in Generic_Data)
persistent from inside a command. (My special case is ad-hoc
overloading, but I think that is irrelevant for the following.)
My current setup is (could you please point out any inadequate choices):
- To set up a command ("adhoc_overloading" in my case) that should also
work inside local contexts I use "Outer_Syntax.local_theory".
- For data related to the command I use "Generic_Data" (since it should
be available in top-level theories as well as local contexts).
- Investigating "notation" a bit (but not understanding the
implementation details ;)), I suspect that "Local_Theory.declaration" is
used to make changes in my "Generic_Data" persistent. What is the
purpose of the "{syntax: bool, pervasive: bool}" argument of
"Local_Theory.declaration".
- "Local_Theory.declaration" expects a "declaration" as argument, which
abbreviates the type "morphism -> Context.generic -> Context.generic".
For the time being I just ignore "morphism" (of course I will have to
understand and incorporate it at some point). So my declaration is
essentially a call to "Context.mapping" which takes two mappings: "f"
for "theory -> theory" and "g" for "Proof.context -> Proof.context".
- So far so good. Everything compiles fine. When I actually use my newly
defined command, I get the error "Stale theory encountered". So
obviously I'm doing something wrong in the above "f" (if I replace "f"
by "I" the error disappears, but of course then I can also not make
changes in my "Generic_Data" persistent.)
- Even if "f" is replaced by "I" above, something I do not understand
happens w.r.t. "g". But this is specific to my "adhoc_overloading" so I
have to give some more details:
adhoc_overloading
foo foo_list
parses "foo" and "foo_list" with "Parse.const" and preprocesses all its
arguments by "Proof_Context.read_const ctxt false dummyT", which I
thought was the canonical way to check whether a string is a (locally
fixed) constant.
Now inside a local context
context
fixes foo_nat :: nat
begin
I try
adhoc_overloading
foo foo_nat
And obtain
Unknown constant: "foo_nat"
When adding some "debug output" to my internal function I obtain the
following before the error:
checking constant: "foo"
const
DONE.
checking constant: "foo_nat"
free
DONE.
checking constant: "foo"
const
DONE.
checking constant: "foo_nat
Unknown constant: "foo_nat"
Which tells me that once "foo_nat" is parsed as a locally fixed constant
(represented by a Free variable) as expected. What I did not expect was
that all the arguments are considered a second time (so actually "g" is
called twice). In this second run we are apparently in a different
context, since "foo_nat" is no longer locally fixed. I'm sure that this
is the correct behavior, but maybe someone could explain it to me.
For completeness find my current adhoc_overloading.ML attached (but be
aware that it is far from finished; it is merely a sandbox in which I
play to find out more about the internals of Isabelle).
Sorry for the lengthy email, but it's really hard to find your way
through the existing Isabelle/ML API without professional help ;)
cheers
chris
On 05/31/2013 06:08 AM, Makarius wrote:
On Wed, 29 May 2013, Florian Haftmann wrote:
Alternatively, use Context.>> directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).
Hypersearch over the sources shows that Context.>> is still quite rare,
and there is no trend to be seen yet. Of course, a trend could be
started now.
Last time we've discussed that privately, you were more in favour of
setup and I more in favour of Context.>> (quite some years ago).
I am myself used to Context.>> in Isabelle/Pure (there is no other way),
and I follow the old habit with 'setup' in Isabelle/HOL most of the time.
On the other hand, the received two-part idiom is a bit odd wrt. proper
modularity:
ML_file "foo.ML"
setup Foo.setup
Like two-component glue to be fit together by hand. It used to be three
components until recently, with extra "uses" in the theory header.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
(* Author: Alexander Krauss, TU Muenchen
Author: Christian Sternagel, University of Innsbruck
Ad-hoc overloading of constants based on their types.
*)
signature ADHOC_OVERLOADING =
sig
val is_overloaded: Context.generic -> string -> bool
val overload: bool -> string -> Context.generic -> Context.generic
val variant: bool -> string -> (string * typ) -> Context.generic ->
Context.generic
val show_overloaded: bool Config.T
end
structure Adhoc_Overloading: ADHOC_OVERLOADING =
struct
val show_overloaded = Attrib.setup_config_bool @{binding show_overloaded} (K
true);
Re: [isabelle-dev] auto raises a TYPE exception
Am 30/05/2013 15:11, schrieb Lawrence Paulson: > I know that there have been a lot of other papers on higher-order unification > expressed as an inference system. Maybe Dale Miller knows more about this > work. I do follow that literature and haven't seen anything relevant on pattern unification. Having had another look at my paper on the algorithm in the clear light of day I realize why: there is no conceptual issue after all. The algorithm does not need the types, it works for untyped terms. Hence the extension to Isabelle's typed terms merely involves unifying types as you go along. I had another look at the code an it seems to do enough type unification, assuming the two start terms have the same type. Hence I must concur with you: although worthwhile, such a verification would not be "significant in a wider context", as you put it. Tobias > Larry > > On 30 May 2013, at 13:04, Tobias Nipkow wrote: > >> >> Am 30/05/2013 13:49, schrieb Tobias Nipkow: >>> Am 30/05/2013 13:41, schrieb Lawrence Paulson: The only question is whether Isabelle is important enough for such work to be seen as significant in a wider context. >>> >>> Makarius is right, the interaction of schematic type variables and HOU has >>> never >>> been nailed down properly and would be of interest to a larger community. >> >> Correction: my CTRS 90 paper contains a pen-and-paper formalisation of the >> full >> HOU algorithm expressed as transformation rules, but without proofs. It is >> the >> pattern unification algorithm where the polymorphic case seems not to have >> been >> examined in any detail (except probably in my head at the time). >> >> Tobias >> >>> 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
There is a funny comment here: http://isabelle.in.tum.de/repos/isabelle/file/cdba0c3cb4c2/src/HOL/Spec_Check/base_generator.ML#l94 (* Isabelle does not use vectors? *) Isn't live nice without vectors, arrays, a host of "int" types that are not int at all? The one exception is src/Pure/Syntax/parser.ML, where arrays are used internally due to some historic "optimization". It probably wastes a lot of space, since every grammar update needs a fresh copy of the whole thing. Working routinely on the JVM now (due to Scala), I've found so many inefficiencies in the libraries due to the historic predominance of these mutable bulk data structures (aka arrays). This is particularly bad when working with plain text, aka strings. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] adhoc overloading
On Wed, 29 May 2013, Florian Haftmann wrote: Alternatively, use Context.>> directly in the body of the ML file (which, I guess, is nowadays preferred over explicit setup in the surrounding theory). Hypersearch over the sources shows that Context.>> is still quite rare, and there is no trend to be seen yet. Of course, a trend could be started now. Last time we've discussed that privately, you were more in favour of setup and I more in favour of Context.>> (quite some years ago). I am myself used to Context.>> in Isabelle/Pure (there is no other way), and I follow the old habit with 'setup' in Isabelle/HOL most of the time. On the other hand, the received two-part idiom is a bit odd wrt. proper modularity: ML_file "foo.ML" setup Foo.setup Like two-component glue to be fit together by hand. It used to be three components until recently, with extra "uses" in the theory header. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On Thu, 30 May 2013, Lukas Bulwahn wrote:
On 05/30/2013 03:51 PM, Makarius wrote:
* Canonical session name? It looks like the name of the tool is
"Spec_Check", according to its main Spec_Check.thy
So it would be session HOL-Spec_Check in ~~/src/HOL/Spec_Check/
Yes, I think Spec_Check is the name to go with.
See 2c893e0c1def ... cdba0c3cb4c2.
The initial 2c893e0c1def is your
https://bitbucket.org/nicolai490/qcheck_tum/commits/f0a79be57a4b and the
final cdba0c3cb4c2 the same after some polishing of Isabelle/ML style.
There were no big problems, just various fine points, and the next student
should have a chance to learn from a tidy situation.
* NEWS and CONTRIBUTORS entries.
Summary and Authors are in the README file from that NEWS and CONTRIBUTORS
can be derived.
That is still left to you. (As usual I've put it on my TODO list for the
next release, just to make sure.)
I was thinking of a ML antiquotation for "check_property @{context}" and I
was thinking of @{spec ...} and some context flags that lets spec either only
compile, or check with values.
This should allow that @{spec ...} could be inlined in the implementation if
anyone wishes to do so.
Looking again how it is done, I don't see the purpose of an antiquotation
-- apart from looking superficially like "annotations" that other people
put into their language.
An Isabelle/ML antiquotation is evaluated at compile-time, in the static
context *before* the compiler works on the whole module. Thus you see
only those ML bindings that were there beforehand, not what you define
within the module itself.
I've done it a bit differently in
http://isabelle.in.tum.de/repos/isabelle/rev/e7c47fe56fbd via some plain
ML function with implicit use of the dynamic compilation context. This
allows to refer to toplevel declarations incrementally, e.g. see the
example with "thy" in
http://isabelle.in.tum.de/repos/isabelle/rev/f22d227a090c.
Another note on http://isabelle.in.tum.de/repos/isabelle/rev/2c141c169624:
Isabelle output is message oriented, i.e. you normally produce just one
piece, not several "lines" sequentially. Nice Isabelle messages use
pretty printing (potentially with extra markup).
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Mira / AFP configuration problem?
We keep getting odd errors like this: Unknown option "parallel_proofs_reuse_timing" e.g. here: http://isabelle.in.tum.de/reports/Isabelle/report/715f292e5d3d4be1b9e1af4be0d136d0 It seems to be some old AFP version that is tested here accidentally. I had parallel_proofs_reuse_timing at some point, but later discontinued it. What is also odd: ML_HOME="/home/polyml/polyml-svn/x86-linux" Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 05/30/2013 05:32 PM, Makarius wrote:
On Thu, 30 May 2013, Lukas Bulwahn wrote:
I was thinking of a ML antiquotation for "check_property @{context}"
and I was thinking of @{spec ...} and some context flags that lets
spec either only compile, or check with values.
This should allow that @{spec ...} could be inlined in the
implementation if anyone wishes to do so.
Do you know how to define the ML antiquotation, or shall I do it?
Please go ahead and do it when you have time.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On Thu, 30 May 2013, Lukas Bulwahn wrote:
I was thinking of a ML antiquotation for "check_property @{context}" and I
was thinking of @{spec ...} and some context flags that lets spec either only
compile, or check with values.
This should allow that @{spec ...} could be inlined in the implementation if
anyone wishes to do so.
Do you know how to define the ML antiquotation, or shall I do it?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On 05/30/2013 03:51 PM, Makarius wrote:
So back to this now:
* Canonical session name? It looks like the name of the tool is
"Spec_Check", according to its main Spec_Check.thy
So it would be session HOL-Spec_Check in ~~/src/HOL/Spec_Check/
You still have a chance to rename "Spec_Check" now, before
anything is
pushed to main Isabelle. The directory location is given by having a
session built on HOL, though.
Yes, I think Spec_Check is the name to go with.
* Formal licensing. As part of the main source tree it implicitly
joins the toplevel LICENSE. It is possible to have a 1-line
add-on in
each theory header, e.g. see ~~/src/HOL/SPARK/SPARK.thy, but not a
separate LICENSE file.
There is no need for a separate LICENSE file here.
The README could also say in plain words that the original code-base
by Christopher League has been relicensed under the 3-clause BSD
license of Isabelle -- i.e. a slightly reduced version of what is in
the README of f0a79be57a4b already.
Yes, I was trying to point this out, but did not state it in such
precise words.
* NEWS and CONTRIBUTORS entries.
Summary and Authors are in the README file from that NEWS and
CONTRIBUTORS can be derived.
Further (less important hints on the README):
3. As Isabelle can run heavily in parallel, we avoid reference types.
Sounds like someone got surprised after 10 years of multicores in the
consumer market that parallel programming is just the normal
situation. When I was a young student, we did learn parallel and
concurrent programming by default, instead of the oo-nonsense that
came on later generations. (Times have changed again already, so we
don't have to revisit this old topic.)
4. Isabelle has special naming conventions and documentation of source
code is only minimal to avoid parroting.
Sounds a bit depressing for me, since I've tried to explain the good
old high-quality code writing techniques in the implementation manual,
and then the young people don't even fit sources on the screen (much
more than the 80--100 char line length). BTW, I've seen really good
sources recently: ACL2. They have a *strict* 80 char limit, and
really good writing style of "essays", not "code documentation".
Anyway, we stick to what Isabelle/ML is, and don't have to make
excuses for it.
These are no excuses, but they simply describe the reasons for the
differences between the original QCheck and the Isabelle's Spec_Check
implementation.
Dou you want to have a toplevel Isar command for "check_property
@{context}"? That is relatively easy to have these days. What should
be its name?
I was thinking of a ML antiquotation for "check_property @{context}"
and I was thinking of @{spec ...} and some context flags that lets spec
either only compile, or check with values.
This should allow that @{spec ...} could be inlined in the
implementation if anyone wishes to do so.
All of this is possible future work, but more importantly, I would like
to see some volunteer that advertises and mentors a follow-up student
project for Spec_Check.
Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Spec_Check
On Thu, 30 May 2013, Lukas Bulwahn wrote:
https://bitbucket.org/nicolai490/qcheck_tum
@Makarius: Are you willing to include the current state in
Isabelle's repository, e.g. under src/Tools/?
The sources are in a stable state and maintenance in last
half year boiled down to only one minor change. Hence, I
believe that it is a low-maintenance part in Isabelle and can
be easily maintained the next few years with almost no
further effort.
"Low-maintenance" does not exist, but this looks indeed nice and clean.
We've actually been close to include it some months ago, but then there
were remaining questions, vacation on my side, move to new job on your
side etc.
So back to this now:
* Canonical session name? It looks like the name of the tool is
"Spec_Check", according to its main Spec_Check.thy
So it would be session HOL-Spec_Check in ~~/src/HOL/Spec_Check/
You still have a chance to rename "Spec_Check" now, before anything is
pushed to main Isabelle. The directory location is given by having a
session built on HOL, though.
* Formal licensing. As part of the main source tree it implicitly
joins the toplevel LICENSE. It is possible to have a 1-line add-on in
each theory header, e.g. see ~~/src/HOL/SPARK/SPARK.thy, but not a
separate LICENSE file.
The README could also say in plain words that the original code-base
by Christopher League has been relicensed under the 3-clause BSD
license of Isabelle -- i.e. a slightly reduced version of what is in
the README of f0a79be57a4b already.
* NEWS and CONTRIBUTORS entries.
Further (less important hints on the README):
3. As Isabelle can run heavily in parallel, we avoid reference types.
Sounds like someone got surprised after 10 years of multicores in the
consumer market that parallel programming is just the normal situation.
When I was a young student, we did learn parallel and concurrent
programming by default, instead of the oo-nonsense that came on later
generations. (Times have changed again already, so we don't have to
revisit this old topic.)
4. Isabelle has special naming conventions and documentation of source
code is only minimal to avoid parroting.
Sounds a bit depressing for me, since I've tried to explain the good old
high-quality code writing techniques in the implementation manual, and
then the young people don't even fit sources on the screen (much more than
the 80--100 char line length). BTW, I've seen really good sources
recently: ACL2. They have a *strict* 80 char limit, and really good
writing style of "essays", not "code documentation".
Anyway, we stick to what Isabelle/ML is, and don't have to make excuses
for it.
Dou you want to have a toplevel Isar command for "check_property
@{context}"? That is relatively easy to have these days. What should be
its name?
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
I know that there have been a lot of other papers on higher-order unification expressed as an inference system. Maybe Dale Miller knows more about this work. Larry On 30 May 2013, at 13:04, Tobias Nipkow wrote: > > Am 30/05/2013 13:49, schrieb Tobias Nipkow: >> Am 30/05/2013 13:41, schrieb Lawrence Paulson: >>> The only question is whether Isabelle is important enough for such work to >>> be seen as significant in a wider context. >> >> Makarius is right, the interaction of schematic type variables and HOU has >> never >> been nailed down properly and would be of interest to a larger community. > > Correction: my CTRS 90 paper contains a pen-and-paper formalisation of the > full > HOU algorithm expressed as transformation rules, but without proofs. It is the > pattern unification algorithm where the polymorphic case seems not to have > been > examined in any detail (except probably in my head at the time). > > Tobias > >> 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Spec_Check
On Thu, 30 May 2013, Lukas Bulwahn wrote: I used the Bavarian holiday today to get the aforementioned Quickcheck tool into a stable state. The latest stable version is at: https://bitbucket.org/nicolai490/qcheck_tum I've started looking, and will come back on this in a few minites. (For now just a fresh mail thread on a fresh topic.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
Hi everyone,
motivated by the current discussion, I used the Bavarian holiday today
to get the aforementioned Quickcheck tool into a stable state.
The latest stable version is at:
https://bitbucket.org/nicolai490/qcheck_tum
I will only have some spare time if at all to maintain it.
I hope someone at TUM is willing to take this over and
mentor a bachelor or master student, who could write
formal specifications for the unification and/or pattern
matching in Isabelle.
I bet quickchecking the specifications with appropriate
generators will uncover more surprises of the current
implementations.
@Makarius: Are you willing to include the current state in
Isabelle's repository, e.g. under src/Tools/?
The sources are in a stable state and maintenance in last
half year boiled down to only one minor change. Hence, I
believe that it is a low-maintenance part in Isabelle and can
be easily maintained the next few years with almost no
further effort.
Lukas
On 05/30/2013 12:23 AM, Tobias Nipkow wrote:
this incident has again reminded me that in the absence of formal proofs about
the code, assertions in the code would be a big step forward. they could have
told us a long time ago that some precondition expected by the unification code
is not guaranteed. lukas and a student had even put together a quickcheck
infrastructure for Isabelle/ML. All of this could be confined to regression
runs. i think we should make some effort in this direction to increase our
confidence in the kernel.
tobias
Am 27/05/2013 19:54, schrieb Makarius:
On Mon, 27 May 2013, Makarius wrote:
The change ensures that variables with equal name are unified, in the same
manner as the types of Free or Const are unified, before doing the real work
of HO-unification.
Here is another example for Isabelle/Pure, without schematic variables with
different types. It may be be tried before/after my change 3b9c31867707 from
today:
ML {* toplevel_pp ["term"] "Proof_Display.pp_term Pure.thy" *}
declare [[show_types]]
typedecl nat
typedecl bool
ML {*
val read = Syntax.read_term (Proof_Context.set_mode
Proof_Context.mode_schematic @{context});
val a = read "a :: nat => bool";
val x = read "?x :: ?'b";
*}
ML {* Seq.list_of (Unify.hounifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
ML {* Seq.list_of (Unify.unifiers (@{theory}, Envir.empty 15, [(a, x)])); *}
ML {* Pattern.unify @{theory} (a, x) (Envir.empty 15); *}
Before the change, Unify.hounifiers crashes; after the change it is able to work
out the type instantiation correctly. Pattern.unify is still not quite there,
neither before nor after the change.
Note that the original implementation by Larry did try to unify the result types
in any case, using the body_type function. But that was assuming that the arity
of the function type happens to coincide with the number of arguments in the
term application.
This is why I introduced optional bounds to the function type traversal in
envir.ML 7f3549a316f4. Note that in 3b9c31867707 the type unification of the
disagreement pair is done explicitly via unify_types_of, without taking the
functions apart, but also see the modification of assignment where these bounds
correspond to the number of actual arguments.
For the moment, I am not going to produce more changes. Maybe Larry and Tobias
also want to comment, as the authors of these modules from some decades ago.
Stefan is of course the proven expert who re-investigated quite a lot of that
around 2000.
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
Re: [isabelle-dev] auto raises a TYPE exception
Am 30/05/2013 13:49, schrieb Tobias Nipkow: > Am 30/05/2013 13:41, schrieb Lawrence Paulson: >> The only question is whether Isabelle is important enough for such work to >> be seen as significant in a wider context. > > Makarius is right, the interaction of schematic type variables and HOU has > never > been nailed down properly and would be of interest to a larger community. Correction: my CTRS 90 paper contains a pen-and-paper formalisation of the full HOU algorithm expressed as transformation rules, but without proofs. It is the pattern unification algorithm where the polymorphic case seems not to have been examined in any detail (except probably in my head at the time). Tobias > 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] auto raises a TYPE exception
Am 30/05/2013 13:41, schrieb Lawrence Paulson: > The only question is whether Isabelle is important enough for such work to be > seen as significant in a wider context. Makarius is right, the interaction of schematic type variables and HOU has never been nailed down properly and would be of interest to a larger community. Tobias ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
There might be a lot of interesting projects that involve verifying parts of our code, and any of these could be beneficial, even if only parts of the code are covered. I guess it would be in the spirit of the recent trend to studying the semantics of real things. The only question is whether Isabelle is important enough for such work to be seen as significant in a wider context. But certainly such work would be good enough to get an MPhil. Larry On 30 May 2013, at 12:13, Tobias Nipkow wrote: > I am not saying we shouldn't prove bits of the code. By all means, do it. But > until you have verified the whole kernel, it just increases some warm feeling > we > have about the code. In this particular case, verification would not have > helped > that much because the problem came from the violation of an unstated > precondition. So in addition to verifying the unification code you have to > verify all calls of it. > > Assertions/testing and verification are complementary, with very different > costs > and benefits. > > Tobias > > > Am 30/05/2013 11:50, schrieb Makarius: >> On Thu, 30 May 2013, Tobias Nipkow wrote: >> >>> this incident has again reminded me that in the absence of formal proofs >>> about >>> the code, assertions in the code would be a big step forward. they could >>> have >>> told us a long time ago that some precondition expected by the unification >>> code is not guaranteed. >> >> Concerning "the code", it really just refers to these two special modules: >> pattern.ML and unify.ML. All the rest has gradually been improved over 20 >> years, so that it does not suffer from any such uncertainty. (Otherwise the >> system would still be the tiny research experiment that it used to be in the >> 1980-ies, not the big thing we have today.) >> >> >>> lukas and a student had even put together a quickcheck infrastructure for >>> Isabelle/ML. All of this could be confined to regression runs. i think we >>> should make some effort in this direction to increase our confidence in the >>> kernel. >> >> When Lucas Buhlwahn started this experiment, I pointed him to pattern.ML and >> unify.ML as the key problem zones. At the same time it was clear that a >> little >> proof-of-concept with quickcheck cannot address the more profound questions >> that >> arise here. >> >> For these particular modules, I would like to see a proper formalization of >> what >> it really is. The question of how schematic polymorphism conceptully >> interacts >> with HO unification does not seem to be resolved after such a long time. >> >> >>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] auto raises a TYPE exception
I am not saying we shouldn't prove bits of the code. By all means, do it. But until you have verified the whole kernel, it just increases some warm feeling we have about the code. In this particular case, verification would not have helped that much because the problem came from the violation of an unstated precondition. So in addition to verifying the unification code you have to verify all calls of it. Assertions/testing and verification are complementary, with very different costs and benefits. Tobias Am 30/05/2013 11:50, schrieb Makarius: > On Thu, 30 May 2013, Tobias Nipkow wrote: > >> this incident has again reminded me that in the absence of formal proofs >> about >> the code, assertions in the code would be a big step forward. they could have >> told us a long time ago that some precondition expected by the unification >> code is not guaranteed. > > Concerning "the code", it really just refers to these two special modules: > pattern.ML and unify.ML. All the rest has gradually been improved over 20 > years, so that it does not suffer from any such uncertainty. (Otherwise the > system would still be the tiny research experiment that it used to be in the > 1980-ies, not the big thing we have today.) > > >> lukas and a student had even put together a quickcheck infrastructure for >> Isabelle/ML. All of this could be confined to regression runs. i think we >> should make some effort in this direction to increase our confidence in the >> kernel. > > When Lucas Buhlwahn started this experiment, I pointed him to pattern.ML and > unify.ML as the key problem zones. At the same time it was clear that a > little > proof-of-concept with quickcheck cannot address the more profound questions > that > arise here. > > For these particular modules, I would like to see a proper formalization of > what > it really is. The question of how schematic polymorphism conceptully > interacts > with HO unification does not seem to be resolved after such a long time. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] auto raises a TYPE exception
On Thu, 30 May 2013, Tobias Nipkow wrote: this incident has again reminded me that in the absence of formal proofs about the code, assertions in the code would be a big step forward. they could have told us a long time ago that some precondition expected by the unification code is not guaranteed. Concerning "the code", it really just refers to these two special modules: pattern.ML and unify.ML. All the rest has gradually been improved over 20 years, so that it does not suffer from any such uncertainty. (Otherwise the system would still be the tiny research experiment that it used to be in the 1980-ies, not the big thing we have today.) lukas and a student had even put together a quickcheck infrastructure for Isabelle/ML. All of this could be confined to regression runs. i think we should make some effort in this direction to increase our confidence in the kernel. When Lucas Buhlwahn started this experiment, I pointed him to pattern.ML and unify.ML as the key problem zones. At the same time it was clear that a little proof-of-concept with quickcheck cannot address the more profound questions that arise here. For these particular modules, I would like to see a proper formalization of what it really is. The question of how schematic polymorphism conceptully interacts with HO unification does not seem to be resolved after such a long time. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
