[Hol-info] hol_light `make' failure with ocaml 3.12.1 camlp5
John, here's my bug report for trying to install the latest ocaml & camlp5. `make' failed in hol_light (error message at the end). I'm an 64 bit Dell Linux box running Scientific Linux: (poisson)ocaml-3.12.1> uname -a Linux poisson.math.northwestern.edu 2.6.32-220.4.1.el6.x86_64 #1 SMP Mon Jan 23 17:20:44 CST 2012 x86_64 x86_64 x86_64 GNU/Linux I untarred ocaml-3.12.1.tar.gz camlp5-6.05.tgz and (poisson)ocaml-3.12.1> ./configure -prefix /rhome/2/richter/HOL-Light (poisson)ocaml-3.12.1> make world > log.world 2>&1 & (poisson)ocaml-3.12.1> make bootstrap > log.bootstrap 2>&1 (poisson)ocaml-3.12.1> make world > log.world 2>&1 & (poisson)ocaml-3.12.1> make bootstrap > log.bootstrap 2>&1 (poisson)ocaml-3.12.1> make opt > log.opt 2>&1 You have mail in /var/spool/mail/richter (poisson)ocaml-3.12.1> make opt.opt make install Seemed to install fine. (poisson)camlp5-6.05> ./configure -prefix /rhome/2/richter/HOL-Light Resulting configuration file (config/Makefile.cnf): MODE=S EXE= OPT=.opt EXT_OBJ=.o EXT_LIB=.a OVERSION=3.12.1 VERSION=6.05 VERSDIR= OTOP=$(TOP)/ocaml_stuff/3.12.1 OCAMLC_W_Y="-w y" WARNERR="-warn-error A" NO_PR_DIR=--no-print-directory OLIBDIR=/rhome/2/richter/HOL-Light/lib/ocaml PREFIX=/rhome/2/richter/HOL-Light BINDIR=$(PREFIX)/bin LIBDIR=$(PREFIX)/lib/ocaml MANDIR=$(PREFIX)/man OCAMLN=ocaml CAMLP5N=camlp5 === strict mode === Strict is the default; I didn't know that. We see ocaml is installed: (poisson)camlp5-6.05> which ocaml /rhome/2/richter/HOL-Light/bin/ocaml (poisson)camlp5-6.05> make world.opt seemed to work fine! Now install: (poisson)camlp5-6.05> make install And it seems to have worked! (poisson)camlp5-6.05> ls $HOME/HOL-Light/bin camlp4* camlp4prof*camlp5sch* ocamlcp* ocamlobjinfo* camlp4boot* camlp4r* mkcamlp4* ocamldebug*ocamlopt* camlp4o*camlp4rf* mkcamlp5* ocamldep* ocamlopt.opt* camlp4of* camlp4rf.opt* mkcamlp5.opt* ocamldep.opt* ocamlprof* camlp4of.opt* camlp4r.opt* ocaml* ocamldoc* ocamlrun* camlp4oof* camlp5*ocamlbuild* ocamldoc.opt* ocamlyacc* camlp4oof.opt* camlp5o* ocamlbuild.byte*ocamllex* ocpp5* camlp4o.opt*camlp5o.opt* ocamlbuild.native* ocamllex.opt* camlp4orf* camlp5r* ocamlc* ocamlmklib* camlp4orf.opt* camlp5r.opt* ocamlc.opt* ocamlmktop* Now I'll build the latest version of HOL Light: (poisson)~> svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light [...] Checked out revision 135. (poisson)hol_light> export LD_LIBRARY_PATH=$HOME/HOL-Light/lib:/rhome/richter/Gambit/current/lib (poisson)hol_light> make (poisson)hol_light> make \ if test `ocamlc -version | cut -c3` = "0" ; \ then cp pa_j_`ocamlc -version | cut -c1-4`.ml pa_j.ml ; \ else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.1" ; \ then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \ else if test `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.2" -o `camlp5 -v 2>&1 | cut -f3 -d' ' | cut -f1-3 -d'.' | cut -c1-6` = "6.02.3" ; \ then cp pa_j_3.1x_6.02.2.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 \ fi \ fi if test `ocamlc -version | cut -c3` = "0" ; \ then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_j.ml; \ else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \ fi File "pa_j.ml", line 195, characters 6-21: Error: The constructor PaLab expects 2 argument(s), but is applied here to 3 argument(s) make: *** [pa_j.cmo] Error 2 I have no idea what that means. Lines 195--7 of pa_j.ml are | PaLab loc x1 x2 -> let loc = floc loc in PaLab loc (self x1) (vala_map (option_map self) x2) I'll go try this at home on an old 32 bit machine. -- Best, Bill -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
[Hol-info] hol_light `make' failure with ocaml 3.12.1 camlp5
John, just to check, on the same machine, I installed the earlier version (ocaml 3.09.1 with presumably camlp4) without any trouble. cd ocaml-3.09.1 ./configure -prefix /rhome/2/richter/HOL-Light309 make world.opt make install I put $HOME/HOL-Light309/bin and $HOME/HOL-Light309/lib on the front of my PATH and LD_LIBRARY_PATH variables. Then cd hol_light make no error, so I ran my miz3 Tarski code hol_light> ocaml #use "hol.ml";; paste in file [] val ( I1_THM ) : thm = |- !a b x y. ~(a = b) ==> ~(x = y) ==> a on_line x,y ==> b on_line x,y ==> x,y equal_line a,b I never get tired of looking that output! -- Best, Bill -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sun, 13 May 2012, Ramana Kumar wrote: > On Sat, May 12, 2012 at 11:54 PM, John Harrison > wrote: > >> | Does this mean unit lists in HOL Light? :) >> | I'm thinking of adding a check that there are no more than 2^30-1 type >> | variables in the input theorem. >> >> I don't exclude either possibility yet... >> > > And what about switching to big integers? (for HOL Zero and/or HOL > Light) I thought HOL Zero might be switching to SML at some point > anyway? With unit list John was probably hoping to have a precise model of natural numbers in OCaml. This is not exactly the case, because datatype values can have loops in that language: let rec uuuh = () :: uuuh;; List.length uuuh;; Anyway, I think we need to find an exit strategy from this endless thread. Already in October 2009, I've tried to convince Mark that OCaml is not the right vehicle for extremely high trustability that he wants to have for HOL Zero. And back then, I did not know all these nasty tricks yet that can be learned in the coffee room of LRI, with hardcore experts like Filiatre showing off all the boundary cases and neat tricks outside the normal mathematics of ML. This is why SML never became very popular, because it spoils these games. Makarius -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Hi John/Ramana,
John Harrison wrote:
> I shouldn't have tempted fate by mentioning you! But I'm not yet
> completely convinced. It's true that it would create a type operator
> with recorded arity 0, but (at least in the HOL Light implementation)
> it would still end up applied to the sorted list of type variables
> ("tyvars") as if it had arity 2^31. That's not to say this is an ideal
> situation, but it seems to fall into the "anomalous" cetegory rather
> than the actually inconsistent. Or am I missing something?
Ah yes, you're absolutely right - the theorem still has the correct arity
and so this is not a route to unsoundness. Phew!
But I still get a fundamental sense of unease that types can be constructed
that are not well-formed (i.e. where the arities are wrong), so I'll adapt
HOL Zero to stop this.
John Harrison wrote:
> Mark wrote:
>> I always thought that this would be impossible to exploit in practice,
>> but now I'm thinking 2^31 =~ 2 billion, and this is perhaps doable ...
>
> Well, I hope that's impossible for pragmatic reasons: wraparound on
> 2^31 would only happen on a 32-bit platform, and then I don't think
> you could address enough memory directly to put this to the test since
> pointers are also 32-bit. And on a 64-bit machine the bar becomes
> much higher because integers won't wrap till 2^63. But perhaps there
> is some weird way of setting up OCaml where pointers are 64-bit but
> type int is 32-bit?
Yes, you're right again. 64-bit machines will have 63-bit integers unless
using special tricks, and 32-bit machines won't be able to address enough
RAM unless using special tricks. So looks like it couldn't be a problem in
practice. (note that my bounty qualification criteria aim to ban what I
mean by "special tricks")
Ramana Kumar wrote:
> And what about switching to big integers? (for HOL Zero and/or HOL Light)
> I thought HOL Zero might be switching to SML at some point anyway?
Yes, big integers is the other possibility. I'm trying to do it as light
weight as possible, and yet keeping the user interface "conventional" (using
the classic types so that integer literals supplied by the user do not have
to be wrapped with 'Int'). However, the HOL Zero natural number syntax
functions already use big integers, and so there is already an inconsistency
in style here, and so maybe I should follow your suggestion. And yes, I
will be switching to SML, but this is several months away, and in any case,
I want everything to be as watertight as possible in the OCaml
implementation.
Mark.
--
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
Ramana Kumar wrote: > Mark wrote: >> Yes, big integers is the other possibility. ... > > Sounds good. > For your information, I am currently working on a verified compiler for > (currently a pure subset of) SML. > But it is also probably several months away from completion :) Yes, I heard about this. Sounds great stuff! Would be nice if it could have some sort of simple mechanism for disallowing overwriting of certain ML and pretty printer bindings (e.g. a compiler directive that could be applied for a given binding, which would set a one-way flag on the binding). This would stop 'thm' and its pretty printer being overwritten by the user, for example, and would be an easy way of eliminating this long-standing vulnerability of LCF-style systems that run in a simple classic top level ML session. Mark. -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sun, May 13, 2012 at 1:07 PM, "Mark" wrote: > Yes, big integers is the other possibility. I'm trying to do it as light > weight as possible, and yet keeping the user interface "conventional" > (using > the classic types so that integer literals supplied by the user do not have > to be wrapped with 'Int'). However, the HOL Zero natural number syntax > functions already use big integers, and so there is already an > inconsistency > in style here, and so maybe I should follow your suggestion. And yes, I > will be switching to SML, but this is several months away, and in any case, > I want everything to be as watertight as possible in the OCaml > implementation. > Sounds good. For your information, I am currently working on a verified compiler for (currently a pure subset of) SML. But it is also probably several months away from completion :) > > Mark. > -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sat, May 12, 2012 at 11:54 PM, John Harrison wrote: > | Does this mean unit lists in HOL Light? :) > | I'm thinking of adding a check that there are no more than 2^30-1 type > | variables in the input theorem. > > I don't exclude either possibility yet... > And what about switching to big integers? (for HOL Zero and/or HOL Light) I thought HOL Zero might be switching to SML at some point anyway? > > John. > > > -- > Live Security Virtual Conference > Exclusive live event will cover all the ways today's security and > threat landscape has changed and how IT managers can respond. Discussions > will include endpoint security, mobile security and the latest in malware > threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ > ___ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > -- Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
