make new dmtcp hets-hollight-tools images for utopic

[cmaeder]

I was not able yet to get this hol-light working using ocaml version 4.01.0

[sternk]

The version of hol-light we are currently using does not work with the newer ocaml version. We will probably have to move to a newer version of hol-light.

[jelmd]

Test wrt. hets-lib/HolLight/example_binom.hol : ubuntu vivid ships 20131026:

> hol-light -version
The OCaml toplevel, version 4.01.0
> hol-light /tmp/example_binom.hol
File "/tmp/example_binom.hol", line 2, characters 1-2:
Error: Syntax error

On Solaris 11 I use 2.20+, i.e. https://github.com/jrh13/hol-light from 20151025 aka latest

> hol-light -version
The Objective Caml toplevel, version 3.11.2
> hol-light /tmp/example_binom.hol 
File "/tmp/example_binom.hol", line 2, characters 1-2:
Error: Syntax error

[sternk]

At first glance it seems to be the same hol-light version we have used previously (the source file hol.ml states ´let hol_version = "2.20++";´" which is the same as in http://www.cl.cam.ac.uk/~jrh13/hol-light/hol_light_100110.tgz

Before digging deeper I will however try if can get the old build process (https://github.com/spechub/Hets/blob/master/HolLight/OcamlTools/Makefile) to work on a recent version of Ubuntu.

[sternk]

Ok - So the problem is not with binom.ml but with the way hol-light was called. Instead of passing binom.ml as an argument the following needs to be entered at the prompt which appears a while after calling hol-light

needs "example_binom.hol";;

which yields

needs "example_binom.hol";;

val binom : thm = |- (!n. binom (n,0) = 1) /\ (!k. binom (0,SUC k) = 0) /\ (!n k. binom (SUC n,SUC k) = binom (n,SUC k) + binom (n,k)) val BINOM_LT : thm = |- !n k. n < k ==> binom (n,k) = 0 val BINOM_REFL : thm = |- !n. binom (n,n) = 1 1 basis elements and 0 critical pairs Translating certificate to HOL inferences val BINOM_FACT : thm = |- !n k. FACT n * FACT k * binom (n + k,k) = FACT (n + k) val it : unit = ()

I'll try to update the build-process to use the installed hol-light and a packaged version of dmtcp.

[sternk]

Branch 1402_hol_light_package should fix this issue. Package has been successfully built on trusty and wily (I'll upload the package for utopic and vivid in a couple minutes) and tested on trusty with the ppa build of Hets.

Update: No package for utopic since this version of Ubuntu 'obsolete' and is thus rejected by Launchpad.

[cmaeder]

I've just tried it under vivid and got:

maeder@lati:~/Hets$ /usr/bin/hets -g HolLight/example_binom.hol 
hets: user error (HolLight.importData: dmtcp_coordinator starting...
    Host: lati (127.0.1.1)
    Port: 7779
    Checkpoint Interval: disabled (checkpoint manually instead)
    Exit on last client: 1
)

and a "mtcp_restart crash with SIGSEGV" Ubuntu splash screen.

[sternk]

Weird. I'll have to investigate that ... On 7 Dec 2015 5:44 p.m., "cmaeder" notifications@github.com wrote:

I've just tried it under vivid and got:

maeder@lati:~/Hets$ /usr/bin/hets -g HolLight/example_binom.hol hets: user error (HolLight.importData: dmtcp_coordinator starting... Host: lati (127.0.1.1) Port: 7779 Checkpoint Interval: disabled (checkpoint manually instead) Exit on last client: 1 )

and a "mtcp_restart crash with SIGSEGV" Ubuntu splash screen.

— Reply to this email directly or view it on GitHub https://github.com/spechub/Hets/issues/1402#issuecomment-162587098.

[cmaeder]

64bit

[jelmd]

Hmmm, I don't know dmtcp very well/how good it is, but I think it is pretty dangerous, to save the process image on one machine and execute it on another, which is possibly wrt. HW/exec env. not the same (e.g. instruction set differs even between x86 based CPUs, 32 vs. 64bit, etc.).

IMHO the only safe way would be, that hets runs at least once the full thing and optionally stores it (if dmtcp is available), and next time if it finds its "precompiled version" (which matches the running hets version) it may use it, otherwise business as usually, i.e. full compilation+run.

Another advantage: the repo doesn't get bloated with 32+MB each time when new images are not created in advance ;-)

[sternk]

While we haven't had any such issues yet this might be due to a lack of use. While reading through the documentation I came up with the following info:

http://dmtcp.sourceforge.net/FAQ.html#migrate - So basically libraries / binaries not compiled in a way such that they can be executed on the target machine are likely to cause problems. We however only use binaries / libraries distributed with Ubuntu so I see no obvious issues here.

Looking at https://realworldocaml.org/v1/en/html/the-compiler-backend-byte-code-and-native-code.html it seems that ocamlrun only generates intermediary code to be executed by a virtual machine so the underlying use of ocaml does not raise any obvious flags either.

I'll get myself setup with a vivid VM and will check if I encounter the same issue (and try to figure out why worked on trusty as opposed to vivid).

As another solution I am open to building the Image on demand. This takes however a significant amount of time so we'd have to figure out at what point in the install-process this should happen.

[jelmd]

As said, not sure about libraries/binaries, but i think that ocaml "compiles" stuff as well, and thus may use e.g. avx registers because they are available on this machine, but can't use it on another, because it doesn't have avx ... Anyway, dmtcp may take care of it ...

AFAIU byte-code vs. native code isn't the point here. dmtcp takes a "RAM-copy" of the running ocaml interpreter (the executable in RAM) including its current state (i.e. stacks and bound libs, and a whole bunch of other stuff). Perhaps swapping it out to disk might be something, which comes close to this ... But yes, perhaps pasting 'needs ...;;' at the end of a hol.ml copy, compile and running the produced exe might still be faster than echo 'needs "...";;' | hol-light

Image on demand: not during install, I meant lazy instantiation, i.e. create it at runtime when it is needed (similar like you would use a cache - which would be here a folder on the disk).

[sternk]

Yes - But stack is just a convention so if libs don't change it should be ok. And it seems ocamlrun does not compile. Nonetheless I will investigate if I encounter the same issue. For some reason my download of Ubuntu is unbearably slow so I'll like test it tomorrow

[sternk]

But if you want we can move to lazy instantiation.

[sternk]

I have encountered the same behaviour as @cmaeder so it is probably a general problem. I'll try to figure out what is wrong.

[sternk]

On Wily I encountered the same problem. Comparing the dmtcp version it seems the package made a large jump from trusty (1.2.5) to vivid (2.3.1). Weirdly building locally using the makefile results in a usable image so the tool-chain seems to be ok. I still think it would be worthwile to test if the older dmtcp fixes this issue.

[cmaeder]

the new https://launchpad.net/~hets/+archive/ubuntu/hets/+files/hets-hollight-tools_20131026-2ubuntu2%7Evivid_amd64.deb still fails with the same message (but without Ubuntu SIGSEGV)

[jelmd]

Yepp, so lazy inst. is probably the safe way to go for now.

However, IMHO a SW designer/admin would still put this on the "solving the wrong problem" list. Usually an application knows its state/what has been calculated/results and thus should be able to serialize this data to a persistent store and just read it, when needed... This would be IMHO much much more efficient, reliable and possibly x-platform compatible than bothering with "RAM-snapshots". Unfortunately ocaml seems not to provide any serialization support out of the box, so probably too much work ??? :(

[sternk]

True. That would be the best approach (and the one I would have chosen had I designed HOLLight). I only used dmtcp because it was suggested as a way to speed up HOLLight. The "official" way is to let hol recalculate all the basic proofs all the time which is very slow. I do not know enough about HOL / Ocaml to be sure how much effort such a fundamental change would take.

[sternk]

To implement the lazy approach we'd have to coordinate the change with a new hets release since the use of dmtcp is hardwired in hets. @cmaeder

[cmaeder]

it used to work in the past when the snapshot image was made with the same version of dmtcp that later runs it.

[jelmd]

Just talked with Till. Since I also don't know Ocaml/HOL good enough to implement serialization, he agrees, that we should go for lazy inst.. IMHO it is the best to decouple it from hets by just invoking a script with corresponding params, which in turn does all the magic needed, so one is able to change it (e.g. if other options pop up) without the need to re-compile hets (also testing might be easier). However, doing it completely within hets is also an alternative/shouldn't be a big problem (but unfortunately my haskell-fu is very limited, so can't help much in this case than).

[sternk]

It will be easiest to stick with the current makefile. I'll implement the necessary changes.

On 11 December 2015 at 16:27, jelmd notifications@github.com wrote:

script with corresponding params, which in turn does all the magic needed, so one is able to change it (e.g. if other options pop up) without the need to