On 07/12/2011 11:15 PM, Florian Haftmann wrote:
Hi Cezary (et al),
first, thanks a lot for your efforts, this is a valuable contribution!
There are a number of obvious things that could
be done with it, like you mention Isabelle settings but also proper
use of
local theories (this would avoid the Stale theory errors), split
conjunction
theorems and look them up separately, etc. However I am not sure there
is enough interest.
The interest, I guess, is there, only the degree of suffering so far has
always been below the critical line.
I totally agree with Makarius that improvements will fall into disrepair
as long as there is no regression test for the imports. Maybe one of
the TUM guys would be willing to invest some time and effort to this?
This doesn't seem so hard once we know how to build all this.
I just tried to redo this to see how it works
$ svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light
$ cd hol_light/Proofrecording/hol_light
$ make
and it failed with
[...]
convert type.ml ...
convert update_database.ml ...
convert wf.ml ...
warning: ignoring 'lemma1' in wf.ml
warning: ignoring 'pth' in wf.ml
warning: ignoring 'pth' in wf.ml
done. 1622 named proofs found.
make: Warning: File `pa_j_3.04.ml' has modification time 0.015 s in the
future
\
if test `ocamlc -version | cut -c3` = "0" ; \
then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \
else cp pa_j_3.1x_`camlp5 -v 2>&1 | cut -f3 -d' ' | cut
-c1`.xx.ml pa_j.ml; \
fi
if test `ocamlc -version | cut -c1-4` = "3.10" -o `ocamlc -version | cut
-c1-4` = "3.11" ; \
then ocamlc -c -pp "camlp5r pa_lexer.cmo
pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \
else ocamlc -c -pp "camlp4r pa_extend.cmo
q_MLast.cmo" -I +camlp4 pa_j.ml; \
fi
File "pa_j.ml", line 104, characters 10-13:
Parse error: "::" or "]" expected after [sem_expr_for_list] (in [expr])
File "pa_j.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2
Any hints?
Also, what is the HOL Light release policy? Is everybody really just
using the svn head?
Alex
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
