Comments (22)
IMHO the platform should be viewed as an object that is fully independent of the current Windows installer (even if it should eventually, hopefully as soon as 8.13, supersede it). So I would say 1.5.0 is a good pick for the first platform release. The platform will still officially be in an experimental state for the first release anyway, so the constraints are somehow more relaxed.
from platform.
@gares : Can you please recommend a tag for Coq-elpi and hierarchy builder for the Coq platform 8.11.2 (I plan to release one as well) and Coq platform 8.12.0? A plain build of coq-elpi from opam does not seem to work even on 8.11.2 - it starts building and successfully installs quite a few prerequisites put the build of coq-elpi itself fails for 8.11.2.
from platform.
Are you building on a memory constrained machine? The version for 8.11 (1.4.x iirc, I'm on vac) runs a test that needs 2+GB. For 8.12 we don't have yet a HB release, only a coq-elpi one (1.5.1).
I should be able to be more precise next week.
from platform.
No, I have tested this with 32 and 128 GB. Maybe the opam files or not up to date.
from platform.
Both 1.4.1 and 1.5.0 should work on 8.11. There is no HB tag using 1.5.0 yet.
Would you mind posting the error? I don't have a laptop to try it out myself.
from platform.
We do have a tag now, 0.10. we may still lack an open package. cc @CohenCyril
from platform.
Thanks - I will do some test runs over the weekend. Missing opam packages are no issue - the Coq platform comes with its own opam patch repo.
from platform.
We now have an opam package as well, and as per coq/coq#12391 Coq 8.12.1 is likely to get these versions as well.
from platform.
Very well - I will test it this week. The platform alpha3 release was still mostly technical and I didn't put much effort into package completeness. Now I will focus on this.
from platform.
@gares : I tried simple "opam install coq-elpi" on the 8.11.2 platform and I get this error:
dune build -p elpi -j 15 @all ; RC=$?; \
( cp -r _build/default/src/.ppcache src/ 2>/dev/null || true ); \
( echo "FLG -ppx './merlinppx.exe --as-ppx --cookie '\''elpi_trace=\"true\"'\'''" >> src/.merlin );\
exit $RC
ppxfindcache_deriving_std src/API.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/API.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/API.pp.ml
ppxfindcache_deriving_std src/compiler.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/compiler.mli --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/compiler.pp.mli
ppxfindcache_deriving_std src/ast.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/ast.mli --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/ast.pp.mli
ppxfindcache_deriving_std src/API.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/API.mli --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/API.pp.mli
ppxfindcache_deriving_std src/data.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/data.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/data.pp.ml
ppxfindcache_deriving_std src/compiler.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/compiler.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/compiler.pp.ml
ppxfindcache_deriving_std src/ast.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_deriving_std src/ast.ml --cache-file src/.ppcache/API.ml --cache-file src/.ppcache/API.mli --cache-file src/.ppcache/util.ml --cache-file src/.ppcache/util.mli --cache-file src/.ppcache/ast.ml --cache-file src/.ppcache/ast.mli --cache-file src/.ppcache/data.ml --cache-file src/.ppcache/compiler.ml --cache-file src/.ppcache/compiler.mli) > _build/default/src/ast.pp.ml
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.ml --ppx-opt --cookie --ppx-opt 'elpi_trace="true"' --cache-file src/.ppcache/runtime_trace_on.ml --cache-file src/.ppcache/runtime_trace_on.mli) > _build/default/src/runtime_trace_on.pp.ml
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.mli --ppx-opt --cookie --ppx-opt 'elpi_trace="false"' --cache-file src/.ppcache/runtime_trace_off.ml --cache-file src/.ppcache/runtime_trace_off.mli) > _build/default/src/runtime_trace_off.pp.mli
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.pp.mli (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_on.mli --ppx-opt --cookie --ppx-opt 'elpi_trace="true"' --cache-file src/.ppcache/runtime_trace_on.ml --cache-file src/.ppcache/runtime_trace_on.mli) > _build/default/src/runtime_trace_on.pp.mli
ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.pp.ml (exit 1)
(cd _build/default && ../install/default/bin/ppxfindcache_elpi_trace_deriving_std src/runtime_trace_off.ml --ppx-opt --cookie --ppx-opt 'elpi_trace="false"' --cache-file src/.ppcache/runtime_trace_off.ml --cache-file src/.ppcache/runtime_trace_off.mli) > _build/default/src/runtime_trace_off.pp.ml
My opam package version list is:
base-bigarray base
base-threads base
base-unix base
cairo2 0.6.1 Binding to Cairo, a 2D Vector Graphics Library
camlp5 7.12 Preprocessor-pretty-printer of OCaml
conf-autoconf 0.1 Virtual package relying on autoconf installation
conf-boost 1 Virtual package relying on boost
conf-cairo 1 Virtual package relying on a Cairo system installation
conf-findutils 1 Virtual package relying on findutils
conf-g++ 1.0 Virtual package relying on the g++ compiler (for C++)
conf-gmp 1 Virtual package relying on a GMP lib system installation
conf-gnome-icon-theme3 0 Virtual package relying on gnome-icon-theme
conf-gtk3 18 Virtual package relying on GTK+ 3
conf-gtksourceview3 0+2 Virtual package relying on a GtkSourceView-3 system installation
conf-m4 1 Virtual package relying on m4
conf-mpfr 2 Virtual package relying on library MPFR installation
conf-pkg-config 1.3 Virtual package relying on pkg-config installation
conf-which 1 Virtual package relying on which
coq 8.11.2 pinned to version 8.11.2
coq-aac-tactics 8.11.0 This Coq plugin provides tactics for rewriting universally quantified equa
coq-bignums 8.11.0 Bignums, the Coq library of arbitrary large numbers
coq-compcert 3.7~coq-platform The CompCert C compiler (using coq-platform supplied version of Flocq)
coq-coquelicot 3.1.0 A Coq formalization of real analysis compatible with the standard library
coq-equations 1.2.3+8.11 A function definition package for Coq
coq-ext-lib 0.11.2 A library of Coq definitions, theorems, and tactics
coq-flocq 3.3.1 A formalization of floating-point arithmetic for the Coq system
coq-gappa 1.4.4 A Coq tactic for discharging goals about floating-point arithmetic and rou
coq-interval 4.0.0 A Coq tactic for proving bounds on real-valued expressions automatically
coq-mathcomp-algebra 1.11.0 Mathematical Components Library on Algebra
coq-mathcomp-bigenough 1.0.0 A small library to do epsilon - N reasonning
coq-mathcomp-character 1.11.0 Mathematical Components Library on character theory
coq-mathcomp-field 1.11.0 Mathematical Components Library on Fields
coq-mathcomp-fingroup 1.11.0 Mathematical Components Library on finite groups
coq-mathcomp-finmap 1.5.0 Finite sets, finite maps, finitely supported functions, orders
coq-mathcomp-real-closed 1.1.1 Mathematical Components Library on real closed fields
coq-mathcomp-solvable 1.11.0 Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect 1.11.0 pinned to version 1.11.0
coq-menhirlib 20190924 A support library for verified Coq parsers produced by Menhir
coq-mtac2 1.1+8.11 Mtac2: Typed Tactics for Coq
coq-quickchick 1.3.2 Randomized Property-Based Testing Plugin for Coq
coq-simple-io 1.3.0 IO monad for Coq
coq-unicoq 1.3+8.11 An enhanced unification algorithm for Coq
coq-vst 2.6 Verified Software Toolchain
coqide 8.11.2 IDE of the Coq formal proof management system
cppo 1.6.6 Code preprocessor like cpp for OCaml
depext transition opam-depext transition package
dune 2.6.2 Fast, portable, and opinionated build system
dune-configurator 2.6.2 Helper library for gathering system configuration
dune-private-libs 2.6.2 Private libraries of Dune
gappa 1.3.5 Tool intended for formally proving properties on numerical programs dealin
lablgtk3 3.0.beta5 pinned to version 3.0.beta5
lablgtk3-sourceview3 3.0.beta6 OCaml interface to GTK+ gtksourceview library
menhir 20190924 An LR(1) parser generator
num 1.3 The legacy Num library for arbitrary-precision integer and rational arithm
ocaml 4.07.1 The OCaml compiler (virtual package)
ocaml-base-compiler 4.07.1 Official release 4.07.1
ocaml-compiler-libs v0.12.1 OCaml compiler libraries repackaged
ocaml-config 1 OCaml Switch Configuration
ocaml-migrate-parsetree 1.7.3 Convert OCaml parsetrees between different versions
ocamlbuild 0.14.0 OCamlbuild is a build system with builtin rules to easily build most OCaml
ocamlfind 1.8.1 A library manager for OCaml
opam-depext 1.1.3 Query and install external dependencies of OPAM packages
ppx_derivers 1.2.1 Shared [@@deriving] plugin registry
ppx_deriving 4.5 Type-driven code generation for OCaml >=4.02.2
ppx_tools 5.1+4.06.0 Tools for authors of ppx rewriters and other syntactic tools
ppxfind 1.4 Tool combining ocamlfind and ppx
ppxlib 0.15.0 Standard library for ppx rewriters
re 1.9.0 RE is a regular expression library for OCaml
result 1.5 Compatibility Result module
seq base Compatibility package for OCaml's standard iterator type starting from 4.0
sexplib0 v0.14.0 Library containing the definition of S-expressions and some base converter
stdlib-shims 0.1.0 Backport some of the new stdlib features to older compiler
from platform.
On the Coq platform 8.12 it is the same. Maybe the OCaml version I use (4.07.1)?
Can you please try the coq platform 8.11 and 8.12 alpha3 scripts - they should run on pretty much any platform with a posix shell now.
The scripts create new opam switches for the coq platform with these names:
_coq-platform_.8.11.2.alpha3
_coq-platform_.8.12.0.alpha3
so they shouldn't change anything in your existing setup.
from platform.
Another test didn't work either:
opam switch create elpi-test ocaml-system.4.08.1
eval $(opam env)
opam repo add coq-released "https://coq.inria.fr/opam/released"
opam install coq-elpi
The following actions will be performed:
- install seq base [required by re]
- install dune 2.6.2 [required by elpi]
- install conf-findutils 1 [required by coq]
- install conf-m4 1 [required by ocamlfind]
- install camlp5 7.12 [required by elpi]
- install stdlib-shims 0.1.0 [required by ppxlib]
- install sexplib0 v0.14.0 [required by ppxlib]
- install result 1.5 [required by ocaml-migrate-parsetree, ppx_deriving]
- install re 1.9.0 [required by elpi]
- install ppx_tools 6.2 [required by ppx_deriving]
- install ppx_derivers 1.2.1 [required by ppx_deriving, ocaml-migrate-parsetree, ppxlib]
- install ocaml-compiler-libs v0.12.1 [required by ppxlib]
- install cppo 1.6.6 [required by ppx_deriving]
- install ocamlfind 1.8.1 [required by coq]
- install ocaml-migrate-parsetree 1.7.3 [required by elpi]
- install num 1.3 [required by coq]
- install ppxlib 0.15.0 [required by elpi]
- install ppxfind 1.4 [required by ppx_deriving]
- install coq 8.12.0 [required by coq-elpi]
- install ppx_deriving 4.5 [required by elpi]
- install elpi 1.11.2 [required by coq-elpi]
- install coq-elpi 1.5.1
===== 22 to install =====
Do you want to continue? [Y/n] Y
:
[ERROR] The compilation of elpi failed at "/Users/msoegtrop/.opam/opam-init/hooks/sandbox.sh build make build
DUNE_OPTS=-p elpi -j 15".
The detailed error messages are as above. I tested this on macOS - in case you think this is a Mac specific sandboxing issue (not unheard of), I can also try it on Linux and Windows - the errors look to unspecific to me to judge this.
from platform.
P.S.: I also tried to disable sandboxing on Mac - this doesn't work either.
from platform.
OK, now some good news: on Linux (Ubuntu 18.04) and Windows it does work both for 8.11.2 and 8.12.0. Any idea what the Mac issue could be? There is not really an error message - it just says "exit 1". Maybe we can have a remote debug session on my Mac.
from platform.
@gares : I debugged this and found that elpi is using "sha1sum". This is not available on mac by default, but can be installed using Macports and homebrew (package name is in both cases md5sha1sum
so one of these commands should work (I tried with MacPorts and it fixes the elpi issue):
sudo port install md5sha1sum
brew install md5sha1sum
How shall we fix this? The options I see are
- create an opam conf package for md5sha1sum with depext support for Mac (on Ubuntu and cygwin it is already installed)
- use something more up to date, say
shasum
oropenssl dgst
. I will check what is available on plain Ubuntu, plain Mac and my coq platform cygwin installation - use an OCaml library for this - I am sure something like this must be available
from platform.
I tested that shasum
is available on the Mac, Linux (Ubuntu 18.04) and Cygwin and it should be functionally identical to sha1sum. I created a PR (LPCIC/elpi#82).
Of cause we can still go with the opam conf option if you want to avoid new tags.
from platform.
Sorry I was one vac and I had no time to read this. Your fix is great!
from platform.
@gares : I have one more issue: CoqElpi does not work in CoqIDE 8.11.2 - I guess you know that since someone fixed it in 8.12.0. My plan is to also publish a Coq platform for Coq 8.11.2 (at the same time as for 8.12.0). Any suggestions what I should do with Elpi:
- not include it in Coq platform 8.11.2
- patch CoqIDE
- put a disclaimer somewhere
In case you are not aware: the following piece of code works in VSCoq 8.11.2 but not in CoqIDE 8.11.2:
From elpi Require Import elpi.
Goal True.
Elpi Tactic show.
Elpi Accumulate lp:{{
solve _ [goal Ctx Proof Type _] _ :-
coq.say "Goal:" Ctx "|-" Proof ":" Type.
}}.
Elpi Typecheck.
elpi show.
from platform.
Hum, is it the parsing of lp:{{ .... }}
that fails?
You can always do Elpi Accumulate " some code "
but then you need to escape "Goal:"
for example, using Coq's string escaping.
I think that at some point I tried to fix CoqIDE (it pre-chops the text looking for .
and this does not work anymore) and failed, so the patch was reverted. I don't recall exactly what fixed it in 8.12.
from platform.
FTR, elpi 1.11.4 which includes your sha1sum fix is released
from platform.
@gares: I added it to the v8.12 branch - you can try it there. Please note that this branch does a full parallel build which requires a bit more than 13 GB of RAM, so you should have at least 16 GB physical (I will add a sequential build option later).
For 8.11 I will add a note displayed after install if CoqIDE and coq-elpi are installed, that CoqIDE does not work with Coq-elpi and that it does work in 8.12.
from platform.
This is fixed meanwhile.
coq-elpi is included in 8.12.2 and 2021.02.0.
I will delay creating of Platforms for older versions of Coq (something which is useful for fighting package bit rot). If I include coq-elpi in such older releases we can see then.
from platform.
Related Issues (20)
- "Argument list too long" error when installing coq-unimath HOT 8
- Add path length check on root path on Windows (for serapi). HOT 1
- CI: update Github actions HOT 2
- snap-installed Coq Platform does not work in emacs/ProofGeneral HOT 3
- coq-platform snap: missing icons in coqide HOT 2
- changed code signature in macOS release 8.17.1~2023.08? HOT 2
- coq_makefile broken
- Tracker issue for 8.18 pick creation
- Scripts: opam update is done to late - it must be done before switch creation
- Add coq-tools / coq-bug-minimizer to the platform? HOT 2
- Add coinduction to the Coq Platform
- Add the libraries for undecidability and first-order logic to the Platform HOT 4
- Coq Platform & OCaml 5 HOT 1
- CI: auto cancel workflow runs on new push to PR branch
- Snap release 8.18 / 2023.11.0 HOT 1
- Missing Windows 32bit binaries in 2023.11.0 release HOT 3
- 2023.11.0 on Mac M2: coq-unicoq, coq-relation-algebra fail with seg fault HOT 14
- README incorrectly says there's no binary release for Apple Silicon HOT 1
- Tracker issue for 8.19 package tag creation
- Please avoid Dune 3.13-3.15 HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from platform.