Hello Freek!
I am trying to get miz3 to run and could use some advice. Here is what I
did so far.
1) miz3 and miz3f are on my path. miz3.ml is in the hol_light directory.
miz3's exrc is sourced in my vimrc.
2) I started ocaml with
ocaml unix.cma
The unix.cma appears to be necessary.
3) In ocaml, I run
#use "hol.ml";;
#use "miz3.ml";;
4) I start gvim and load a file with the following content:
let ARITHMETIC_SUM = thm ';
!n. nsum(1..n) (\i. i) = (n*(n+1)) DIV 2
proof
qed by #INDUCT_TAC;
';;
5) Then I press Control-C Return.
As far as I understand your paper, the generated subgoals should now be
inserted in the file. However, what happens instead is the following:
* The vim buffer does not change and no error is reported.
* In the ocaml repl, the following error message appears:
# File "/tmp/miz3_2545.ml", line 1, characters 25-26:
Parse error: ';;' or [use_file] expected after [str_item] (in [use_file])
Error in included file /tmp/miz3_2545.ml
Could you tell me what is going on? I tried to make sure that the file is
exactly as given in your paper.
Thanks!
Felix
2012/4/25 Freek Wiedijk <[email protected]>
> Dear everyone,
>
> John Harrison pointed out to me that the following query was
> posted on the hol-info mailing list (I'm subscribed to that
> list but often just delete the messages without looking,
> sorry about that. So I missed this):
>
> >6) I am very curious about Mizar Light and would like to convert
> >my exercise to Mizar Light. I found the Mizar Light sources as
> >well Freek's paper on Mizar Light. However, at first glance it
> >seemed as if the syntax for Mizar Light given in the paper is
> >quite different from what I saw in the source. So... what is the
> >current status of the project?
>
> There have been three experiments that I called "Mizar
> Light". However, after some soal searching I decided to
> rename the third thing from "Mizar Light III" to "miz3",
> so please don't call this third version Mizar Light
> anymore... :-)
>
> 1. The first thing is described in a TPHOLs paper from
> 2001, <http://www.cs.ru.nl/~freek/mizar/miz.pdf>.
> _Conceptually,_ I still _really_ like this, but
> ergonomically it's completely unusable, because of all
> the quotes and brackets, and because it's really hard
> to debug proofs. The Mizar proof
>
> Lm1: P implies P
> proof
> assume P;
> hence P;
> end;
>
> becomes in this framework:
>
> let lm1 = prove
> (`P ==> P`,
> ASSUME_A(0,`P:bool`) THEN
> THUS(`P:bool`) (BY [0][]));;
>
> 2. The second version never has been published about, but
> is part of the HOL Light distribution, it is in the
> sub-directory "Mizarlight". It is an attempt to make
> the first version more ergonomic, while still keeping
> the property that a proof is just ocaml code, so without
> having a separate "Mizar parser". In this system the
> above proof becomes:
>
> let lm1 = theorem
> "P ==> P"
> [assume "P";
> hence "P"];;
>
> 3. And then there's my recent "miz3" system, which
> is my current best effort, and which (very similar to
> John Harrison's "Mizar mode") _does_ have a separate
> parser that allows one to get really close to
> Mizar syntax. It's described in the recent paper
> <http://www.cs.ru.nl/~freek/miz3/miz3.pdf>,
> and the system can be downloaded as
> <http://www.cs.ru.nl/~freek/miz3/miz3.tar.gz>. In this
> system the example is:
>
> let lm1 = thm `;
> let P be bool;
> thus P ==> P
> proof
> assume P;
> thus P;
> end`;;
>
> (In miz3 all variables have to be bound, either in the
> formula or in the context, hence the "let" at the start.
> Also in miz3 "then" is implicit, hence the "thus"
> instead of the "hence".)
>
> I hope this clears things up. I guess the poster might
> have been confused between the first and second, or second
> and third version of the thing?
>
> Ah yes, and if someone would like help with using miz3,
> just mail me!
>
> Freek
>
>
> ------------------------------------------------------------------------------
> 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
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
http://www.felixbreuer.net
------------------------------------------------------------------------------
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
