Thank you for taking the time to look into this.
I agree that a Cygwin poly/ml version is the best route to a Windows build
(Moscow ML is simply too slow for serious work).
Initially, I’d be happy to not use the Holmake code that depends on Posix.
Instead, we could use the Moscow ML approach, and just have single-threaded
Holmake. If there’s an easy way to emulate the fork/exec approach that Holmake
exploits on Unix, then that would be better of course.
As you say, the core of the system is pretty pure SML and should work just fine
on Windows.
Best wishes,
Michael
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Date: Wednesday, 18 January 2017 at 01:24
To: "Norrish, Michael (Data61, Canberra City)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] PAT_ASSUM doesn't remove the assumption now? (and a
theorem cannot be proved in K11 any more)
Sorry, I re-checked my Isabelle environment and found that the PolyML in
Isabelle is actually built by GCC (mingw versions), so my statement about
"PolyML cannot be built in ..." was completely wrong. The rest ideas should
still hold.
On 17 January 2017 at 13:36, Chun Tian (binghe)
<binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>> wrote:
No, it’s actually my pleasure to make a little contribution.
For the Windows build issue, I think the correct path is to try to build HOL
using the PolyML (32bit and 64bit) and Cygwin environment shipped with
Isabelle2016-1 (installed on Windows 10). This version of PolyML is built by
Visual Studio 2010, it has normal executions, DLLs and other files, the
structure looks exactly like those we manually build on Linux and Mac. PolyML
cannot be built in Mingw32 or Cygwin32 using GCC compilers, thus trying to
build HOL in pure Cygwin environment results into failure. So we can expect
the final HOL build should be able to run standalone in Windows CMD shell, if
this plan works. MosML shouldn’t be considered at all.
I ever tried to make some initial fixes. The most obvious issue is that, HOL’s
ML code used functions from the “Posix” structure, but this structure is not
available on Windows. Some of these unavailable functions can be found in OS
structure, which is available on all platforms. Others may need to be manually
implemented on Windows using functions from OS or Windows structures. Also,
when detecting the location of executions, HOL’s ML code doesn’t consider
“.exe” as part of file name at all. These are all minor issues is irrelevant to
the theorem proving related code. However, I’m not an experienced ML
programmer (I’m actually a Common Lisp programmer), can’t do complex ML coding
at current moment …
On 17 January 2017 at 00:23,
<michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>> wrote:
If you are using the working copy of HOL from the git repository, you should
check the release notes in HOLDIR/doc. We document major incompatibilities
there.
Note also that the last official release was K10. There is a tag for K11 in
the repository, and some release notes for it, but it hasn’t been released due
to issues with the Windows build. The change to PAT_ASSUM is documented in
doc/next-release.md<http://next-release.md>, which will eventually be renamed
to the K12 release notes in all likelihood.
The working repo did not have corrected .doc files for those functions though,
so thank you very much for writing those!
Michael
On 17/1/17, 05:47, "Chun Tian (binghe)"
<binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>> wrote:
Hi,
HOL Reference said that, PAT_ASSUM "Finds the first assumption that matches
the term argument, applies the theorem tactic to it, and removes this
assumption.” But I found it actually doesn’t remove the assumption in latest
Kananaskis 11.
To see this, try the following goal (open listTheory first):
> g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
:
proofs
First I rewrite it:
> e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
OK..
1 subgoal:
val it =
FILTER ($= x) l = [x]
------------------------------------
0. ∀x.
(x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
1. MEM x l
:
proof
Then I want to pick the assumption 0 and specialize the quantifier with `x`:
> e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
<<HOL message: inventing new type variable names: 'a>>
OK..
1 subgoal:
val it =
((x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
(FILTER ($= x) l = [x])
------------------------------------
0. ∀x.
(x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
1. MEM x l
:
proof
>
Now you can see, the assumption 0 is still here. It’s not removed as the
manual said.
In Kananaskis 10, the behavior is exactly the same as described in the
manual:
- g `!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l`;
<<HOL message: inventing new type variable names: 'a>>
> val it =
Proof manager status: 1 proof.
1. Incomplete goalstack:
Initial goal:
∀l. ALL_DISTINCT (h::l) ⇒ ALL_DISTINCT l
: proofs
- e (RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM]);
OK..
1 subgoal:
> val it =
FILTER ($= x) l = [x]
------------------------------------
0. ∀x.
(x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
1. MEM x l
: proof
- e (PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`));
<<HOL message: inventing new type variable names: 'a>>
OK..
1 subgoal:
> val it =
((x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
(FILTER ($= x) l = [x])
------------------------------------
MEM x l
: proof
See, the used assumption has been removed.
Now let’s insist that, the behavior in latest Kananaskis 11 is more
reasonable (thus we should update the manual), because later we may be able to
use the assumption again for another different purpose. Now to finish the
proof, in Kananaskis 10 a single rewrite almost finish the job using theorem
FILTER_NEQ_NIL:
- FILTER_NEQ_NIL;
> val it =
|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x
: thm
- e (RW_TAC std_ss [FILTER_NEQ_NIL]);
OK..
1 subgoal:
> val it =
MEM h l
------------------------------------
MEM h l
: proof
Now the goal is the same as the only assumption left:
- e (FIRST_ASSUM ACCEPT_TAC);
OK..
Goal proved.
[.] |- MEM h l
Goal proved.
[.]
|- ((x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])) ⇒
(FILTER ($= x) l = [x])
Goal proved.
[..] |- FILTER ($= x) l = [x]
But in Kananaskis 11 the same tactical cannot prove the theorem any more:
> FILTER_NEQ_NIL;
val it =
|- ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x:
thm
> e (RW_TAC std_ss [FILTER_NEQ_NIL]);
OK..
1 subgoal:
val it =
FILTER ($= x) l = [x]
------------------------------------
0. ∀x.
(x = h) ∨ MEM x l ⇒
((if x = h then h::FILTER ($= h) l else FILTER ($= x) l) = [x])
1. MEM x l
:
proof
In fact we’re going back to previous status before PAT_ASSUM was used! In
short words, the following theorem definition doesn’t work any more: (it works
in Kananaskis 10)
(* BROKEN !!! *)
val ALL_DISTINCT_CONS = store_thm("ALL_DISTINCT_CONS",
``!l. ALL_DISTINCT (h::l) ==> ALL_DISTINCT l``,
RW_TAC std_ss [ALL_DISTINCT_FILTER,FILTER,MEM] THEN
PAT_ASSUM ``!y. P`` (MP_TAC o Q.SPEC `x`) THEN
RW_TAC std_ss [FILTER_NEQ_NIL] THEN
FIRST_ASSUM ACCEPT_TAC);
Could anyone please explain these strange behaviors and point out a correct
way to prove this theorem? (it’s actually part of the HOL-ACL2 bridge, defined
in “examples/acl2/ml/fmap_encodeScript.sml”)
Best regards,
Chun Tian
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>
https://lists.sourceforge.net/lists/listinfo/hol-info
--
---
Chun Tian (binghe)
University of Bologna (Italy)
--
---
Chun Tian (binghe)
University of Bologna (Italy)
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
