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
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
On 28 May 2013, at 19:52, Makarius makar...@sketis.net 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
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
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
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
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.
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
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
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
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).
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.
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
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.
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
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
16 matches
Mail list logo
