Packages hol_light (including flyspeck's formal_ineqs) and dependency camlp5

[mkoeppe]

Experimental package for the HOL Light theorem prover (http://www.cl.cam.ac.uk/~jrh13/hol-light/), which includes the flyspeck project's formal verifier of nonlinear inequalities (https://github.com/monadius/formal_ineqs).

Assuming distribution package for OCaml is available. Tested on Homebrew (brew install ocaml-num), which has version 4.06.1.

Adding package camlp5. The package available in Homebrew does not seem to work for HOL light, probably because it has not been built in strict mode (https://github.com/jrh13/hol-light/blob/master/README)

(cd upstream && wget https://github.com/camlp5/camlp5/archive/rel705.tar.gz -O camlp5-7.05.tar.gz )

Adding package hol_light. Upstream has no releases. For now we pull directly from their git. Alternatively, could use Debian's .orig.tar.gz (https://packages.debian.org/stretch/hol-light) as our upstream.

hol_light includes formal_ineqs from the Flyspeck project. Original source release without version number at https://github.com/flyspeck/flyspeck/tree/master/downloads, current development said to be at https://github.com/monadius/formal_ineqs, which has some fixes for newer HOL Light.

To use (see https://github.com/monadius/formal_ineqs/blob/master/docs/FormalVerifier.pdf):

$ sage -sh
$ hol-light
# load_path := "SAGE_LOCAL/share/formal_ineqs" :: !load_path ;; 
# needs "verifier/m_verifier_main.hl";;

... this compiles for ca. 40 minutes.

... and gives an error:

- : unit = ()
File "misc/misc_vars.hl" already loaded
- : unit = ()
File "_none_", line 1:
Error: Unbound module Taylor_interval
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/verifier/m_verifier_build.hl
- : unit = ()
File "_none_", line 1:
Error: Unbound module Taylor_interval
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/verifier/m_verifier.hl
- : unit = ()
File "verifier/m_verifier_build.hl" already loaded
- : unit = ()
File "taylor/m_taylor.hl" already loaded
- : unit = ()
File "misc/misc_vars.hl" already loaded
- : unit = ()
File "_none_", line 1:
Error: Unbound module Taylor_interval
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/taylor/m_taylor_arith.hl
- : unit = ()
File "_none_", line 1:
Error: Unbound module Taylor_interval
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/taylor/m_taylor_arith2.hl
- : unit = ()
File "misc/misc_vars.hl" already loaded
- : unit = ()
File "verifier/certificate.hl" already loaded
- : unit = ()
File "informal/informal_taylor.hl" already loaded
- : unit = ()
File "verifier/certificate.hl" already loaded
- : unit = ()
File "verifier_options.hl" already loaded
- : unit = ()
module Informal_search :
  sig
    type search_options = {
      raw_intervals0 : bool;
      max_width : float;
      max_depth : int;
      mono_depth : int;
      pp : int;
    }
    val find_max : 'a list -> 'a * int
    val split_domain :
      int ->
      int ->
      Informal_taylor.m_cell_domain ->
      Informal_taylor.m_cell_domain * Informal_taylor.m_cell_domain
    val restrict_domain :
      int ->
      bool -> Informal_taylor.m_cell_domain -> Informal_taylor.m_cell_domain
    type function_info = {
      eval0 :
        int ->
        Informal_float.ifloat list ->
        Informal_float.ifloat list -> Informal_interval.interval;
      taylor :
        int ->
        int ->
        Informal_taylor.m_cell_domain -> Informal_taylor.m_taylor_interval;
      index : int;
    }
    type result =
        Cell_inconclusive
      | Cell_false
      | Cell_result of Certificate.result_tree
      | Cell_pass of bool * function_info
    exception Construction_error of string * Informal_taylor.m_cell_domain *
                function_info list
    val error :
      string -> Informal_taylor.m_cell_domain -> function_info list -> 'a
    val init_vol : Informal_taylor.m_cell_domain -> unit
    val update_verified_vol : Informal_taylor.m_cell_domain -> unit
    val check_cell :
      search_options ->
      Informal_taylor.m_cell_domain -> function_info list -> result
    val try_mono :
      search_options ->
      Informal_taylor.m_cell_domain ->
      function_info -> Informal_taylor.m_taylor_interval -> result
    val construct_certificate0 :
      search_options ->
      Informal_taylor.m_cell_domain ->
      function_info list -> Certificate.result_tree
    val construct_certificate :
      search_options ->
      Informal_taylor.m_cell_domain ->
      ((int ->
        Informal_float.ifloat list ->
        Informal_float.ifloat list -> Informal_interval.interval) *
       (int ->
        int ->
        Informal_taylor.m_cell_domain -> Informal_taylor.m_taylor_interval))
      list -> Certificate.result_tree
  end
- : unit = ()
File "informal/informal_verifier.hl" already loaded
- : unit = ()
File "_none_", line 1:
Error: Unbound module Eval_interval
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/verifier/m_verifier_main.hl
val it : unit = ()
# File "_none_", line 1:
Error: Unbound module M_verifier_main

Other open questions:

• Can it be compiled with ocamlopt?
• Use checkpointing tool on Linux? On macOS?

Component: packages: experimental

Branch/Commit: u/mkoeppe/package_hol_light__and_dependency_camlp5_ @ b4357f9

Issue created by migration from https://trac.sagemath.org/ticket/25347

[mkoeppe]

Branch: u/mkoeppe/package_hol_light__and_dependency_camlp5_

[mkoeppe]

Commit: 3deb258

[mkoeppe]

New commits:

3deb258

Experimental packages for hol-light, camlp5

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

f8b0680	Experimental packages for hol-light, camlp5
9b9db06	Add package flyspeck_formal_ineqs

[sagetrac-git]

Changed commit from 3deb258 to 9b9db06

[mkoeppe]

comment:5

Earliest error:

Exception: Failure "tryfind".
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/hol-light/Multivariate/realanalysis.ml
- : unit = ()
File "/Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/trig/series.hl", line 318, characters 55-84:
Error: Unbound value REAL_INTEGRABLE_UNIFORM_LIMIT
Error in included file /Users/mkoeppe/s/sage/some-sage-install-prefix/share/formal_ineqs/trig/series.hl
- : unit = ()
File "_none_", line 1:
Error: Unbound module Series

[jdemeyer]

comment:7

Just a comment on the installer scripts: you should use the sdh_... functions (grep for sdh_make_install for example).

[jdemeyer]

comment:8

I don't really like how you pull from git at install time. Better just make a proper package from the git repo. For script packages, there is no dependency or version checking.

And even if you do want to pull from git, this is really bad:

if [ -n "${FORMAL_INEQS_COMMIT}" ]; then
    git checkout ${FORMAL_INEQS_COMMIT}
else
    git pull --ff-only
fi

You really should fix a commit, not just pull whatever is on the master branch.

(NOTE: for experimental packages, you can do whatever you want. So take these comments as advice, not as a requirement)

[mkoeppe]

comment:9

Thanks for the comments; yes, these are very preliminary scripts and before I would set this ticket to review, it would be replaced by using a tarball.

[mkoeppe]

comment:10

Loading Formal_ineqs also fails in Debian's version of the package. https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=898514

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

b4357f9

Remove separate package flyspeck_formal_ineqs because hol_light includes it

[sagetrac-git]

Changed commit from 9b9db06 to b4357f9