From a1b7f53a68c9ccae637f2c357fbe50a09e211a4a Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 24 Jan 2019 14:58:38 +0000 Subject: Dockerfile: update menhir from 20180530 to 20181113 --- dev/ci/docker/bionic_coq/Dockerfile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dev') diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index baf470e021..4cd7faf757 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-12-14-V1" +# CACHEKEY: "bionic_coq-V2019-01-28-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.05.0" # `num` does not have a version number as the right version to install varies # with the compiler version. ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \ - CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" + CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" -- cgit v1.2.3 From e43b1768d0f8399f426b92f4dfe31955daceb1a4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 16 Feb 2018 01:02:17 +0100 Subject: Primitive integers This work makes it possible to take advantage of a compact representation for integers in the entire system, as opposed to only in some reduction machines. It is useful for heavily computational applications, where even constructing terms is not possible without such a representation. Concretely, it replaces part of the retroknowledge machinery with a primitive construction for integers in terms, and introduces a kind of FFI which maps constants to operators (on integers). Properties of these operators are expressed as explicit axioms, whereas they were hidden in the retroknowledge-based approach. This has been presented at the Coq workshop and some Coq Working Groups, and has been used by various groups for STM trace checking, computational analysis, etc. Contributions by Guillaume Bertholon and Pierre Roux Co-authored-by: Benjamin Grégoire Co-authored-by: Vincent Laporte --- dev/top_printers.ml | 4 ++++ dev/vm_printers.ml | 1 + 2 files changed, 5 insertions(+) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 8f207d1e0a..2629cf8626 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -292,6 +292,8 @@ let constr_display csr = ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") then (";"^i) else "")) lna "")^"," ^(array_display bl)^")" + | Int i -> + "Int("^(Uint63.to_string i)^")" and array_display v = "[|"^ @@ -421,6 +423,8 @@ let print_pure_constr csr = print_cut(); done in print_string"{"; print_fix (); print_string"}" + | Int i -> + print_string ("Int("^(Uint63.to_string i)^")") and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index ea126e2756..dc30793a6e 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -82,6 +82,7 @@ and ppwhd whd = | Vcofix _ -> print_string "cofix" | Vconstr_const i -> print_string "C(";print_int i;print_string")" | Vconstr_block b -> ppvblock b + | Vint64 i -> printf "int64(%LiL)" i | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s -- cgit v1.2.3 From 191e253d1d1ebd6c76c63b3d83f4228e46196a6e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 5 Mar 2018 11:09:51 +0100 Subject: Overlays. --- dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh (limited to 'dev') diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh new file mode 100644 index 0000000000..6e89741e29 --- /dev/null +++ b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then + + bignums_CI_REF=primitive-integers + bignums_CI_GITURL=https://github.com/vbgl/bignums + + mtac2_CI_REF=primitive-integers + mtac2_CI_GITURL=https://github.com/vbgl/Mtac2 + +fi -- cgit v1.2.3