Re: [isabelle-dev] adhoc overloading
Dear Florian,
On 05/30/2013 06:03 AM, Florian Haftmann wrote:
Hi Christian,
- For Overload_Data instead of Theory_Data, I should use Generic_Data
(such that it is available in top-level theories and local theories).
Currently that means that I do the following in the setup (where
Adhoc_Overloading.setup is now of type "Context.generic ->
Context.generic").
setup {* fn thy =>
Adhoc_Overloading.setup (Context.Theory thy)
Context.theory_of *}
This looks strange, I'm sure I'm doing something wrong / non-canonical.
I think Adhoc_Overloading.setup should stay theory -> theory: this is
the installation of the necessary syntax check phases, which is done
once globally on import of the corresponding theory – unlike the dynamic
addition via add_overloaded and add_variant
Sorry, my question should have been: how to apply a function of type
"Generic.context -> Generic.context" in a situation where "theory ->
theory" is expected (the former type comes from using Generic_Data, and
the latter is what "setup" should have). In the meanwhile I found
Context.theory_map: (Context.generic -> Context.generic) -> theory ->
theory
Alternatively, use Context.>> directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).
Thanks for the hint. I'm now using "Context.>>" instead of a setup
function called from a thy-file.
- Apparently "constants" (in the sense of locally fixed variables of a
local theory) are represented as "term"s rather than "string"s (in the
notation command). In adhoc_overloading.ML, until now we used "string"s
to represent top-level constants. A change (if really necessary) implies
the following questions:
It depends how far you want to push the game.
* The simplest one I can imagine is to stay on the »constant as string«
level, but have declarations within local theories; if these would be
morphed e.g. due to interpretation, they would only be kept if their
resulting shape is again a constant.
* Treat one component as general term appropriately (maybe the variant?).
* Treat both components as general term appropriately.
My naive approach was to just turn the previous Symtabs into Termtabs,
i.e., previously:
internalize : (string * typ) list Symtab.table
(*maps overloaded constants to lists of variants (together with their
type)*)
externalize : string Symtab.table
(*maps variants to corresponding overloaded constants*)
(An aside: I'm leaning towards renaming those two tables and related
functions as follows:
internalize ~> variant_tab
externalize ~> oconst_tab
which would make more sense to me, but maybe the old naming has a
Isabelle-specific reason I'm not aware of?)
As a first attempt I just changed this into
variant_tab : term list Termtab.table (*we can get the type of a term*)
oconst_tab : term Termtab.table
But of course that is not what I intended, since types are now also
inspected when looking up a key in a table, but at least for overloaded
constants only their name is important. This seems to point towards one
of your first two suggestions. The first one, would require the least
amount of changes (and would allow to print readable error messages).
The question is whether I'm asking for problems, when I treat "Free"
variables (i.e., "constants" in local theories) and "Const"s both as
strings? Any opinions?
A related question. Until now I can only register overloaded constants
and variants via the ML interface, since the "adhoc_overloading" command
I implemented does not seem to effect the surrounding theory. I will
have a look at "notation" again to see how functions of type
"local_theory -> local_theory" are able to make "non-local" changes
persistent, i.e., update the tables in my Generic_Data. Maybe somebody
does already have suggestions in that respect?
cheers
chris
* How to print a "constant" represented as "term" in the error
messages inside Overload_Data (I do not see how I could access the
context here)
Good question. Note that most »fully localized« data store prefer
Item_Net.T as store index, where merge always seems to prefer on branch
(I only did skim over the sources, so this conclusion might be erroneous).
* I also would like to add the possibility to remove overloading and
variants again. Is that against some monotonicity requirement I'm not
aware of?
It should work, with the usual problems on the theory level that things
deleted in one theory come up again after merge with another theory with
partly shared but different ancestry.
- Concerning syntax, I thought about providing commands like:
adhoc_overloading
bind bind_list bind_option and
permute permute_list permute_option
(which would declare "bind" and "permute" as ad-hoc overloaded and add
the variants "bind_list" and "bind_option", and "permute_list" and
"permute_option", respectively.) Maybe some punctuation between the
overloaded constant and
Re: [isabelle-dev] auto raises a TYPE exception
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
Re: [isabelle-dev] Obsolete numeral experiments?
On Tue, 28 May 2013, Makarius wrote: On Tue, 28 May 2013, Brian Huffman wrote: As for Binary.thy, I believe that all the main ideas there have already been incorporated into the HOL numerals library, so there's no reason not to delete it. OK, so I will delete just my old experiment Binary.thy. I've done that now in 0d3165844048, after spending time beforehand to update it to changes in print translation interfaces. (Just the usual renovation before demolition.) 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 Wed, 29 May 2013, Makarius wrote:
Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at
the very end, due to divergence of types of certain Vars, types that
cannot be unified. This is very odd, but should not be a problem at the
moment: Metis should work as before.
Just for completeness, here is the original crash of Metis proof
reconstruction at Isabelle/0fa3b456a267:
lemma ex_tl: "EX ys. tl ys = xs"
using tl.simps(2) by fast
lemma "(∃ys∷nat list. tl ys = xs) ∧ (∃bs∷int list. tl bs = as)"
by (metis ex_tl)
Metis: Failed to replay Metis proof
inst_inference: ("COMP", 1,
["Meson.skolem (Meson.COMBK (tl ((?MesonSK_0_0_0_ys1∷nat
list ⇒ nat list) (xs∷nat \
list)) = xs) (0∷nat)) ⟹
tl ((?MesonSK_0_0_0_ys1∷int list ⇒ int list)
(?MesonV_0_1_0_xs1∷int list)) = (as\
∷int list) ⟹ False"
[.],
"PROP ?psi2 ⟹ PROP ?psi2"])
The failure of COMP is via cterm_instantiate/instantiate_normalize: after
the instantiation, there are ?ys1 of different types, so the extra type
unification of Vars in COMP will fail.
(Note that the pretty-printed exception content is produced via regular
and documented @{make_string} sneaked into the proper spot in the ML code,
without committing that. Many people only know the "secret"
PolyML.makestring, with its unformatted text-only output.)
In 6ba76ad4e679 this crash is avoided: already incremented composition
problems omit the extra type unification, just like plain resolution. This
merely pushed the inherent problem elsewhere, so in 568b2cd65d50
resolve_inc_tyvars is back where types of equal Vars are *not* unified,
despite its lengthy workaround for exactly that.
Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] "interpret ... for a" leaks a
Hi Lars, > in 40fe6b80b481, I stumbled upon the following behaviour. Consider > the following example: > > locale Foo = fixes a :: 'a > > notepad begin > interpret Foo b for b . > term b > end > > jEdit tells me about b in the term command: > > term > fixed "b" > skolem variable > :: 'b > > So the b from the "for b" is leaked into the surrounding context. As all > the lemmas about b where generalized, I would have expected that > b does not become fixed in the surrounding context. I guess the for-parameters are not dealt as expected by interpret. Maybe this is a co-phenomenon of the following warning from isar-ref: > interpret expr where eqns interprets expr in the proof context and is > otherwise similar to interpretation in local theories. Note that rewrite > rules given to interpret after the where keyword should be explicitly > universally quantified. Cheers, Florian Haftmann -- 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
Re: [isabelle-dev] [isabelle] Duplicate constant declaration in sublocale
Hi Lars,
> I have locale A, B and I want to declare B as a sublocale of A. In doing
> so, some of the constants in A can be replaced by simpler ones. I tried
> to use the same names first, but got the following error from the
> sublocale command:
>
> Duplicate constant declaration "local.g" vs. "local.g"
>
> This is not to surprising. However, if I change the definition of g in B
> by removing the explicit type annotation (or use some other type
> variable there), the sublocale command succeeds (of course, this is not
> a solution to my problem, because I want to have exactly the specified
> type for my constant).
maybe in the future this a solution to your problem:
> record ('a,'b) rec =
> proj :: "'b ⇒ 'a"
>
> locale A = fixes G :: "('a, 'b) rec" begin
>
> definition g :: "'a ⇒ 'b ⇒ bool" where
> "g u e = (proj G e = u)"
>
> end
>
> locale B = fixes dummy :: 'a begin
>
> definition "to_rec = ⦇ proj = (fst :: 'a × 'a ⇒ 'a) ⦈"
>
> definition g :: "'a ⇒ ('a × 'a) ⇒ bool" where
> "g u e ⟷ fst e = u"
>
> lemma [simp]: "proj to_rec = fst" by (auto simp: to_rec_def)
>
> lemma [simp]:
> "A.g to_rec = g"
> by (auto simp: g_def A.g_def fun_eq_iff to_rec_def)
>
> interpretation foo: A to_rec
> where
> "proj to_rec = fst" and
> "A.g to_rec = B.g"
> apply unfold_locales
> apply auto
> done
>
> lemmas bar = foo.g_def
I.e. do an interpretation confined to the surface context and then
cherry-pick the lemmas you want.
Cheers,
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
Re: [isabelle-dev] adhoc overloading
Hi Christian,
> - For Overload_Data instead of Theory_Data, I should use Generic_Data
> (such that it is available in top-level theories and local theories).
> Currently that means that I do the following in the setup (where
> Adhoc_Overloading.setup is now of type "Context.generic ->
> Context.generic").
>
> setup {* fn thy =>
> Adhoc_Overloading.setup (Context.Theory thy)
> Context.theory_of *}
>
> This looks strange, I'm sure I'm doing something wrong / non-canonical.
I think Adhoc_Overloading.setup should stay theory -> theory: this is
the installation of the necessary syntax check phases, which is done
once globally on import of the corresponding theory – unlike the dynamic
addition via add_overloaded and add_variant
Alternatively, use Context.>> directly in the body of the ML file
(which, I guess, is nowadays preferred over explicit setup in the
surrounding theory).
> - Apparently "constants" (in the sense of locally fixed variables of a
> local theory) are represented as "term"s rather than "string"s (in the
> notation command). In adhoc_overloading.ML, until now we used "string"s
> to represent top-level constants. A change (if really necessary) implies
> the following questions:
It depends how far you want to push the game.
* The simplest one I can imagine is to stay on the »constant as string«
level, but have declarations within local theories; if these would be
morphed e.g. due to interpretation, they would only be kept if their
resulting shape is again a constant.
* Treat one component as general term appropriately (maybe the variant?).
* Treat both components as general term appropriately.
> * How to print a "constant" represented as "term" in the error
> messages inside Overload_Data (I do not see how I could access the
> context here)
Good question. Note that most »fully localized« data store prefer
Item_Net.T as store index, where merge always seems to prefer on branch
(I only did skim over the sources, so this conclusion might be erroneous).
> * I also would like to add the possibility to remove overloading and
> variants again. Is that against some monotonicity requirement I'm not
> aware of?
It should work, with the usual problems on the theory level that things
deleted in one theory come up again after merge with another theory with
partly shared but different ancestry.
> - Concerning syntax, I thought about providing commands like:
>
> adhoc_overloading
> bind bind_list bind_option and
> permute permute_list permute_option
>
> (which would declare "bind" and "permute" as ad-hoc overloaded and add
> the variants "bind_list" and "bind_option", and "permute_list" and
> "permute_option", respectively.) Maybe some punctuation between the
> overloaded constant and its variant would increase readability?
Maybe \ / => similar to existing syntax things=
> - In the check and uncheck functions I now would have to unify typed
> terms instead of mere constants. Could that be too expensive to be
> practicable?
I have no particular idea about that.
Cheers,
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
Re: [isabelle-dev] auto raises a TYPE exception
On Tue, 28 May 2013, Makarius wrote:
* No change to unify.ML (and especially pattern.ML, which was not really
covered so far). My 3b9c31867707 is backed-out.
* Instead Thm.bicompose_aux in the non-lifted case (i.e. the "compose"
variants) ensures that the types of all Vars are unified
beforehand. So mentioning some ?x::?'a here and some ?x::nat=>bool
there means they become both ?x::nat=>bool before entering
Unify.unifiers (and Pattern.unify as well).
Thus we acknowledge the observation that the old code from 25 years ago
does not work with Vars of different type: Stefan's check from 2005
raises suitable exceptions, and the above pre-stage avoids that this
happens.
I've done this now in c4264f71dc3b .. 568b2cd65d50. The main thing is
0fa3b456a267 to "unify types of schematic variables in non-lifted case".
This was rather trivial, but there were some surprises nonetheless: Metis
proof reconstruction seems to require the non-unification of types of
Vars, despite having a separate workaround for exactly that problem
(see resolve_inc_tyvars in 568b2cd65d50).
Without the latter, src/HOL/Metis_Examples/Clausification.thy crashes at
the very end, due to divergence of types of certain Vars, types that
cannot be unified. This is very odd, but should not be a problem at the
moment: Metis should work as before.
If any of the experts on Metis proof reconstruction want to clean that up:
Thm.bicompose {incremented = false, ...} means types get unified, while
{incremented = true, ...} means there is no need for it since variables
have been incremented as for resolution. If it works one day without the
extra toggle, we can simplify the low-level Thm.bicompose once again. (And
all these "compose" variants are definitely outside normal user space.)
Anyway, apart from having seen a lot of boundary cases of the unification
code -- things we've seen more often in distant past -- the conclusion is
inconclusive. The system cannot be changed substantially at its very
bottom, but we knew that already.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] ML antiquotations: let, note
Hi Christian,
> from `isabelle doc implementation` it is not clear to me what the
> purpose of the two ML antiquotations @{let ...} and @{note ...} is.
> Grepping over Isabelle's sources reveals that those are only used in the
> manual itself. Could anybody clarify?
A small example:
ML {*
@{let ?f = "distinct :: 'a list ⇒ bool"}
@{term "?f [1, 2, 3 :: nat]"};
@{note foo = distinct.simps [where ?'a = "int \ bool"]}
@{thms foo};
*}
A little bit clearer? ;-)
> On a related note, I did not understand the description of the special
> non-ASCII braces in the same part of the manual.
To my understanding, those braces denote logical scopes / subcontexts
similarly to { … } in Isar.
I guess these things still need some time to get commonly used…
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
Re: [isabelle-dev] Obsolete numeral experiments?
>> http://isabelle.in.tum.de/repos/isabelle/file/6324f30e23b6/src/HOL/ex/Binary.thy >> http://isabelle.in.tum.de/repos/isabelle/file/6324f30e23b6/src/HOL/ex/Numeral_Representation.thy >> >> Can we delete that, and keep the history inside the history? Or are there >> remaining aspects that are not in the official numeral implementation (and >> reform) by Brian Huffman? > > Numeral_Representation.thy defines a couple of type classes for > subtraction that were never added to the main libraries: > semiring_minus and semiring_1_minus. (I believe these were Florian's > work.) They would let us generalize some rules that are currently > specific to nat. We should discuss whether these (or some variation) > would be appropriate to add to Groups.thy before we delete > Numeral_Representation.thy. I have some plans in the drawer to introduce / refine type classes for »confined subtraction« coverting natural numbers and multisets. There I will reconsider semiring_minus and semiring_1_minus. The remainder of the theory indeed is obsolete. I guess there are subtle and not so subtle differences between that concept and the now existing implementation, but I do not worry much about that, since the implementation resolves the ancient central problem of signed numerals and is just working. 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
Re: [isabelle-dev] Segmentation faults
From that crash log it looks as though the crash happened in ML code rather than the run-time system itself. The source of the crash, though, could be a bug in the run-time system resulting in some addresses being mangled. It's difficult to say more without being able to reproduce it. David On 29/05/2013 14:03, Lawrence Paulson wrote: Following Dave Matthew's instructions, I downloaded a fresh copy of the sources and executed the following commands. Except the first one failed, presumably because I had a fresh copy. make distclean ./configure --disable-shared make make install I have just taken a look at the crash logs, and it's clear that some dynamic libraries from a previous installation had got loaded along with the latest ones. Maybe that was the problem. I wonder how they got loaded in the first place? I have just deleted them and I hope it will work now. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
Here for example: > Thread 0:: Dispatch queue: com.apple.main-thread > 0 libsystem_kernel.dylib0x99c998e2 __psynch_cvwait + 10 > 1 libsystem_c.dylib 0x984db280 _pthread_cond_wait + 833 > 2 libsystem_c.dylib 0x985610e0 > pthread_cond_timedwait$UNIX2003 + 70 > 3 libpolyml.4.dylib 0x005b37a1 PCondVar::WaitFor(PLock*, > unsigned int) + 113 > 4 libpolyml.4.dylib 0x005c3614 > Processes::BeginRootThread(PolyObject*) + 852 > 5 libpolyml.4.dylib 0x005b7e18 polymain + 2392 The dynamic libraries had an earlier creation date from the other poly/ML libraries. Larry On 29 May 2013, at 14:18, Makarius wrote: > On Wed, 29 May 2013, Lawrence Paulson wrote: > >> I have just taken a look at the crash logs, and it's clear that some dynamic >> libraries from a previous installation had got loaded along with the latest >> ones. > > Where did you see that in the log? > > There is the following near the end, but it looks fine so far: > > Binary Images: >0x1000 - 0x56aff7 +poly (???) <7513623B-C8EF-B2EE-7AB8-86D56D558A10> > /Users/USER/*/poly > 0x59b000 - 0x5fbfeb +libpolyml.4.dylib (5) > <2E0AD632-82FD-C839-A4EF-7C7D917E4C07> /Users/USER/*/libpolyml.4.dylib > 0x110 - 0x1102fff +libsha1.so (0) > /Users/USER/*/libsha1.so > > > Maybe /Users/USER/* is just some anonymized version of the real locations. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
On Wed, 29 May 2013, Lawrence Paulson wrote: I have just taken a look at the crash logs, and it's clear that some dynamic libraries from a previous installation had got loaded along with the latest ones. Where did you see that in the log? There is the following near the end, but it looks fine so far: Binary Images: 0x1000 - 0x56aff7 +poly (???) <7513623B-C8EF-B2EE-7AB8-86D56D558A10> /Users/USER/*/poly 0x59b000 - 0x5fbfeb +libpolyml.4.dylib (5) <2E0AD632-82FD-C839-A4EF-7C7D917E4C07> /Users/USER/*/libpolyml.4.dylib 0x110 - 0x1102fff +libsha1.so (0) /Users/USER/*/libsha1.so Maybe /Users/USER/* is just some anonymized version of the real locations. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
Following Dave Matthew's instructions, I downloaded a fresh copy of the sources and executed the following commands. Except the first one failed, presumably because I had a fresh copy. make distclean ./configure --disable-shared make make install I have just taken a look at the crash logs, and it's clear that some dynamic libraries from a previous installation had got loaded along with the latest ones. Maybe that was the problem. I wonder how they got loaded in the first place? I have just deleted them and I hope it will work now. Larry poly_2013-05-28-145613_epicure.crash Description: Binary data On 29 May 2013, at 10:25, Makarius wrote: > On Tue, 28 May 2013, Lawrence Paulson wrote: > >> It clearly isn't a hardware failure. For one thing, it happens in the same >> way on two separate machines, and anyway, a hardware failure wouldn't affect >> only one specific program. David Matthews thought the problem may be the >> presence of a separate Poly/ML compiler, which I use for MetiTarski work. > > Cqn you explain how this separate Poly/ML is compiled, and where it is > installed? > > >> He thought perhaps the libraries could be interfering. > > The Mac OS X crash report should tell you about the shared libraries that > were used in the failed process. > > There is also "otool -L" to check that statically on the executable, but I am > unsure if it is exactly that. E.g. for polyml-5.5.0-3/x86-darwin/poly from > our Isabelle component it always shows the location where the binary was > compiled originally, regardless of DYLD_LIBRARY_PATH at run-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 28 May 2013, at 19:52, Makarius wrote: > ... you do type unification of Free/Const/Bound incrementally as you go. So > some ?x::'?a could become a function indirectly, e.g. by unifying c::'?a with > c::nat=>bool elsewhere. This is never done, as far as I know. It is known to be intractable. > How about this alternative approach: > > * No change to unify.ML (and especially pattern.ML, which was not really >covered so far). My 3b9c31867707 is backed-out. > > * Instead Thm.bicompose_aux in the non-lifted case (i.e. the "compose" >variants) ensures that the types of all Vars are unified >beforehand. So mentioning some ?x::?'a here and some ?x::nat=>bool >there means they become both ?x::nat=>bool before entering >Unify.unifiers (and Pattern.unify as well). > > Thus we acknowledge the observation that the old code from 25 years ago does > not work with Vars of different type: Stefan's check from 2005 raises > suitable exceptions, and the above pre-stage avoids that this happens. This approach sounds safer anyway. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
On Wed, 29 May 2013, Makarius wrote:
He thought perhaps the libraries could be interfering.
The Mac OS X crash report should tell you about the shared libraries that
were used in the failed process.
There is also "otool -L" to check that statically on the executable, but I am
unsure if it is exactly that. E.g. for polyml-5.5.0-3/x86-darwin/poly from
our Isabelle component it always shows the location where the binary was
compiled originally, regardless of DYLD_LIBRARY_PATH at run-time.
Here is another approach to get this information:
DYLD_PRINT_LIBRARIES=true before the executable is run.
See the included ch-test to change lib/scripts/run-polyml accordingly. The
result looks like this on my Mountain Lion:
$ isabelle tty
dyld: loaded:
/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin/poly
dyld: loaded:
/Volumes/Macintosh_HD/Users/makarius/.isabelle/contrib/polyml-5.5.0-3/x86-darwin/libpolyml.4.dylib
dyld: loaded: /usr/lib/libSystem.B.dylib
dyld: loaded: /usr/lib/libstdc++.6.dylib
dyld: loaded: /usr/lib/system/libcache.dylib
dyld: loaded: /usr/lib/system/libcommonCrypto.dylib
dyld: loaded: /usr/lib/system/libcompiler_rt.dylib
...
Makarius# HG changeset patch
# User wenzelm
# Date 1369820188 -7200
# Node ID 6c3763f05f59feecc81f31f4818abdbbe9468cd9
# Parent c8ee9c0a3a648eee62f7f25b541a8cdf38cd1c96
test;
diff -r c8ee9c0a3a64 -r 6c3763f05f59 lib/scripts/run-polyml
--- a/lib/scripts/run-polymlWed May 29 11:06:38 2013 +0200
+++ b/lib/scripts/run-polymlWed May 29 11:36:28 2013 +0200
@@ -41,7 +41,6 @@
librarypath "$POLYLIB"
-
## prepare databases
if [ -z "$INFILE" ]; then
@@ -74,7 +73,7 @@
fi
"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS
| \
- { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit
"$RC"; }
+ { read FPID; env DYLD_PRINT_LIBRARIES=true "$POLY" -q $ML_OPTIONS; RC="$?";
kill -TERM "$FPID"; exit "$RC"; }
RC="$?"
[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Segmentation faults
On Tue, 28 May 2013, Lawrence Paulson wrote: It clearly isn't a hardware failure. For one thing, it happens in the same way on two separate machines, and anyway, a hardware failure wouldn't affect only one specific program. David Matthews thought the problem may be the presence of a separate Poly/ML compiler, which I use for MetiTarski work. Cqn you explain how this separate Poly/ML is compiled, and where it is installed? He thought perhaps the libraries could be interfering. The Mac OS X crash report should tell you about the shared libraries that were used in the failed process. There is also "otool -L" to check that statically on the executable, but I am unsure if it is exactly that. E.g. for polyml-5.5.0-3/x86-darwin/poly from our Isabelle component it always shows the location where the binary was compiled originally, regardless of DYLD_LIBRARY_PATH at run-time. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
