Re: [isabelle-dev] Modest proposal for image tagging
On 07/12/2011 01:18 PM, Makarius wrote: On Tue, 12 Jul 2011, Alexander Krauss wrote: sed -i 's/THE_VERSION/$(hg id)/g' version.ML isabelle usedir ... Actually, a similar thing happens when an isabelle distribution is built from a repository clone. Alex needs to do this because he his crunching on the official sources. Just to avoid misunderstandings: I am not doing this, but was referring to the makedist script: http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/Admin/makedist#l171. The mira framework works more like approach B), as it keeps metadata in its own database. val my_id = getenv MY_ID; In the latter case you have your own settings (potentially via user components with etc/settings) to ensure that the environment variable is present at build time. This is probably the easiest approach discussed so far. Alex ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] [isabelle] Status of HOL/Import
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 21 | 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
Re: [isabelle-dev] [isabelle] Status of HOL/Import
On Wed, Jul 13, 2011 at 4:51 PM, Alexander Krauss kra...@in.tum.de wrote: On 07/12/2011 11:15 PM, Florian Haftmann wrote: 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 [...] The issue is with versions of OCaml. The HOL Light distribution includes a number of versions of the parser (files pa_j_XXX.ml) that are supposed to work with particular versions of OCaml. I am using an old version of OCaml for HOL Light (3.10.2) however the distribution includes some pa_j_ files for versions 3.11.XXX. Also make sure that camlp5 has the same version as ocaml; as this is not the case for example on macbroys. One more suggestions, try to run 'make' in the top directory of hol light first; after this works you can copy pa_j.ml and pa_j.cm* to ProofRecodring/hollight. Also, what is the HOL Light release policy? Is everybody really just using the svn head? Last named release (2.20) was in 2005, since then John Harrison sometimes packs versions considered more stable. Otherwise it is the SVN. Cezary ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Occur-Check Problem in Isabelle
Guten Abend,
bin Studenten an der Goethe-Uni in Frankfurt und beschäftige mich sehr stark
mit dem Isabelle Beweis-System.
Zur Zeit sitze ich an folgendem Problem in Isabelle.
In dem Lemma subst_no_occ komme ich nicht weiter, ich vermute stark, dass
ich in den Funktionen apply_subst und occ etwas wichtiges übersehen habe
und im Beweis etwas verloren geht.
primrec apply_subst_list :: ('a trm) list \Rightarrow 'a subst \Rightarrow
('a trm) list and
apply_subst :: 'a trm \Rightarrow 'a subst \Rightarrow 'a trm
(infixl \triangleleft 60) where
apply_subst_list [] s = []
| apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)
| (Var v) \triangleleft s = assoc v (Var v) s
| (Fn f xs) \triangleleft s = (Fn f (apply_subst_list xs s))
primrec occ :: 'a trm \Rightarrow 'a trm \Rightarrow bool and
occ_list :: 'a trm \Rightarrow 'a trm list \Rightarrow bool where
occ u (Var v) = False
| occ u (Fn f xs) = (if (list_ex (eq u) xs) then True else (occ_list u
xs))
| occ_list u [] = False
| occ_list u (x#xs) = (if occ u x then True else occ_list u xs)
lemma subst_no_occ: \neg occ (Var v) t \Longrightarrow Var v \neq t
\Longrightarrow t \triangleleft [(v,s)] = t
apply(induct t)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
done
Liebe Grüße
Anja Gerbes
Good evening,
I am student at Goethe University in Frankfurt and I am working with the
Isabelle proof system.
Currently I am sitting at the following problem in Isabelle.
In the lemma subst_no_occ I get no further, I strongly suspect that I am in
the functionsapply_subst and occ have overlooked something important and
something gets lost in the proof.
primrec apply_subst_list :: ('a trm) list \Rightarrow 'a subst \Rightarrow
('a trm) list and
apply_subst :: 'a trm \Rightarrow 'a subst \Rightarrow 'a trm
(infixl \triangleleft 60) where
apply_subst_list [] s = []
| apply_subst_list (x#xs) s = (apply_subst x s)#(apply_subst_list xs s)
| (Var v) \triangleleft s = assoc v (Var v) s
| (Fn f xs) \triangleleft s = (Fn f (apply_subst_list xs s))
primrec occ :: 'a trm \Rightarrow 'a trm \Rightarrow bool and
occ_list :: 'a trm \Rightarrow 'a trm list \Rightarrow bool where
occ u (Var v) = False
| occ u (Fn f xs) = (if (list_ex (eq u) xs) then True else (occ_list u
xs))
| occ_list u [] = False
| occ_list u (x#xs) = (if occ u x then True else occ_list u xs)
lemma subst_no_occ: \neg occ (Var v) t \Longrightarrow Var v \neq t
\Longrightarrow t \triangleleft [(v,s)] = t
apply(induct t)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
done
Greetings
Anja Gerbes
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
