[isabelle-dev] [isabelle] Status of HOL/Import

[Alexander Krauss]

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