pkg/55988: lang/coq: request to update to dune build system and latest release

To: pkg-manager%netbsd.org@localhost,gnats-admin%netbsd.org@localhost,pkgsrc-bugs%netbsd.org@localhost
Subject: pkg/55988: lang/coq: request to update to dune build system and latest release
From: aza.sea.agenda%gmail.com@localhost
Date: Thu, 11 Feb 2021 08:15:01 +0000 (UTC)
>Number:         55988
>Category:       pkg
>Synopsis:       lang/coq: request to update to dune build system and latest release
>Confidential:   no
>Severity:       serious
>Priority:       medium
>Responsible:    pkg-manager
>State:          open
>Class:          change-request
>Submitter-Id:   net
>Arrival-Date:   Thu Feb 11 08:15:00 +0000 2021
>Originator:     Aleksey Arens
>Release:        pkgsrc-trunk
>Organization:
>Environment:
NetBSD HOSTNAME_REDACTED 9.99.79 NetBSD 9.99.79 (GENERIC.STAGING.02) #6: Mon Feb  8 21:36:37 UTC 2021  root@HOSTNAME_REDACTED:/usr/obj/sys/arch/amd64/compile/GENERIC amd64
>Description:
The version of coq in lang/coq at this time is 8.12.2, and it uses a configure+makefile based build system.  For almost a decade, there has been a trend in the OCaml ecosystem to use a new local packaging system -- opam -- and a new build system -- first jbuilder, and subsequently dune.  The use of the latter has a number of advantages, in particular with its ability to intelligently compute dependencies and also to intelligently manage build process.

The latest release of coq, versioned 8.13.0 has a working dune build setup.  I would like to request that the build instructions for the lang/coq package be adjusted to take advantage of the dune build system.

The basic instructions for the use of a dune build system are already encoded into pkgsrc.

I have been able to produce a working dune-based build of coq on NetBSD using opam system, in my home directory.  The following configuration was used:

---8<---

opam-version: "2.0"
synopsis: "Formal proof management system"
description: """
The Coq proof assistant provides a formal language to write
mathematical definitions, executable algorithms, and theorems, together
with an environment for semi-interactive development of machine-checked
proofs. Typical applications include the certification of properties of programming
languages (e.g., the CompCert compiler certification project and the
Bedrock verified low-level programming library), the formalization of
mathematics (e.g., the full formalization of the Feit-Thompson theorem
and homotopy type theory) and teaching."""
maintainer: "coqdev%inria.fr@localhost"
authors: "The Coq development team, INRIA, CNRS, and contributors."
license: "LGPL-2.1-only"
homepage: "https://coq.inria.fr/";
bug-reports: "https://github.com/coq/coq/issues";
depends: [
  "ocaml" {>= "4.05.0"}
  "ocamlfind" {build}
  "num"
  "conf-findutils" {build}
  "zarith" {>= "1.10"}
]
depopts: ["coq-native"]
build: ["dune" "build" "-p" "coq"]
dev-repo: "git+https://github.com/coq/coq.git";
extra-files: [
  "coq.install"
  "sha512=b501737b4dbd22adc1c0377d744448056fb1dc493caf72c05f57c8463cf23f758373605ab3a50b9f505e4c856c41039d0bd7f81f96ed62adc6a674179523e7d2"
]
url {
  src: "https://github.com/coq/coq/archive/V8.13.0.tar.gz";
}


---8<--

These instructions had resulted in a successful build, both on Debian and NetBSD boxes.  In both cases, the following basic functionality test was performed.  The coqtop binary was fed a particular script (cf. https://github.com/coq/coq/issues/7829#issuecomment-776722003 to learn how the use of this particular script emerged), and its behaviour was observed.  The expected outcome has been that the binary would not produce an error, and finish evaluation of the script within 10 seconds.


---8<---
Set Coqtop Exit On Error.
Set Warnings "+default".
Unset Coqtop Exit On Error.
Set Warnings "default".
Goal False.
  change_no_check True.
  exact I.
Qed.
Abort All.
Set Coqtop Exit On Error.
Set Warnings "+default".
Unset Coqtop Exit On Error.
Set Warnings "default".
Goal True -> False.
  intro H.
  change_no_check False in H.
  exact H.
Qed.
Abort All.
Set Coqtop Exit On Error.
Set Warnings "+default".
Unset Coqtop Exit On Error.
Set Warnings "default".
Goal 0 <= 1.
unfold le.
Abort All.
Set Coqtop Exit On Error.
Set Warnings "+default".
Unset Coqtop Exit On Error.
Set Warnings "default".
Opaque Nat.add.
Goal 1 + 0 = 1.
unfold Nat.add.
Abort All.
Set Coqtop Exit On Error.
Set Warnings "+default".
Goal ~0=0.
unfold not.
Fail progress fold not.
pattern (0 = 0).
fold not.
Abort All.
Reset Initial.
Set Coqtop Exit On Error.
Set Warnings "+default".
Opaque id.
Goal id 10 = 10.
Fail unfold id.
with_strategy transparent [id] unfold id.
Abort All.
Reset Initial.
Set Coqtop Exit On Error.
Set Warnings "+default".
Fixpoint fact (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' => n * fact n'
  end.
Strategy 1000 [id].
Goal True.
Time assert (id (fact 8) = fact 8) by reflexivity.
Time assert (id (fact 9) = fact 9) by reflexivity.
---8<---

I used the following Makefile to build coq under pkgsrc with dune:

---8<---
# $NetBSD: Makefile,v 1.136 2020/11/05 09:08:33 ryoon Exp $
#

DISTNAME=	coq-8.13.0
PKGREVISION=	0
CATEGORIES=	lang math
MASTER_SITES=	${MASTER_SITE_GITHUB:=coq/}
GITHUB_TAG=	V${PKGVERSION_NOREV:S/_/+/}

MAINTAINER=	jaapb%NetBSD.org@localhost
HOMEPAGE=	https://coq.inria.fr/
COMMENT=	Theorem prover which extracts programs from proofs
LICENSE=	gnu-lgpl-v2.1

WRKSRC=		${WRKDIR}/${GITHUB_PROJECT}-${PKGVERSION_NOREV:S/+/-/}

USE_TOOLS+=		bash
USE_TOOLS+=		gmake
# # HAS_CONFIGURE=		yes
# CONFIGURE_ARGS+=	-prefix ${PREFIX}
# #CONFIGURE_ARGS+=	-emacslib ${PREFIX}/share/emacs/site-lisp
# CONFIGURE_ARGS+=	-mandir ${PREFIX}/${PKGMANDIR}
# CONFIGURE_ARGS+=	-configdir ${PKG_SYSCONFDIR}/xdg/coq
# CONFIGURE_ARGS+=	-docdir ${PREFIX}/share/doc/coq
# CONFIGURE_ARGS+=	-coqdocdir ${PREFIX}/share/texmf-dist/tex/latex/coq
# CONFIGURE_ARGS+=	-flambda-opts '-O3 -unbox-closures'

BUILDLINK_API_DEPENDS.ocaml+=	ocaml>=4.05.0


UNLIMIT_RESOURCES+=	stacksize
UNLIMIT_RESOURCES+=	datasize
UNLIMIT_RESOURCES+=	cputime
UNLIMIT_RESOURCES+=	virtualsize

# PLIST_VARS+=		native
# .if ${OCAML_USE_OPT_COMPILER} == "yes"
# COQIDE_TYPE=		opt
# PLIST.native=		yes
# CONFIGURE_ARGS+=	-native-compiler yes
# UNLIMIT_RESOURCES+=	stacksize # compilation of some files needs this
# BUILD_TARGET=		world
# .else
# COQIDE_TYPE=		byte
# CONFIGURE_ARGS+=	-native-compiler no
# BUILD_TARGET=		byte
# INSTALL_TARGET=		install-byte
# .endif
# PLIST_SUBST+=		COQIDE_TYPE=${COQIDE_TYPE}

.if (${MACHINE_ARCH} == "i386") || (${MACHINE_ARCH} == "x86_64")
.  if !empty(MACHINE_PLATFORM:MLinux-*-*) || \
      !empty(MACHINE_PLATFORM:MDragonFly-*-*) || \
      !empty(MACHINE_PLATFORM:MFreeBSD-*-*) || \
      !empty(MACHINE_PLATFORM:MDarwin-*-*) || \
      !empty(MACHINE_PLATFORM:MNetBSD-*-*)
PLIST.natdynlink=	yes
.  endif
.endif

.include "../../lang/python/pyversion.mk"

# Sets correct path to python executable.  Actually unused, if doc option is not enabled.
SUBST_CLASSES+=		python
SUBST_STAGE.python=	pre-configure
SUBST_FILES.python=	configure.ml
SUBST_SED.python=	-e 's,@@PYTHON@@,${PYTHONBIN},g'

# Sets correct path to sphinx-build executable.  Actually unused, if doc option is not
# enabled.
SUBST_CLASSES+=		py-sphinx-build
SUBST_STAGE.py-sphinx-build= pre-configure
SUBST_FILES.py-sphinx-build= \
			configure.ml \
			doc/dune
SUBST_SED.py-sphinx-build= -e 's,@@SPHINX_BUILD@@,sphinx-build-${PYVERSSUFFIX},g'

REPLACE_INTERPRETER=	python
REPLACE.python.old=	python3
REPLACE.python.new=	${PYTHONBIN}
REPLACE_FILES.python=	tools/TimeFileMaker.py \
			tools/make-both-single-timing-files.py \
			tools/make-both-time-files.py \
			tools/make-one-time-file.py \
			dev/tools/github-check-prs.py \
			dev/tools/update-compat.py \
			doc/sphinx/conf.py \
			doc/tools/coqrst/regen_readme.py

INSTALL_ENV+=		COQINSTALLPREFIX=${DESTDIR}

PLIST_VARS+=		coqide natdynlink doc

OCAML_USE_DUNE=		yes
DUNE_BUILD_PACKAGES+=	coq
DUNE_BUILD_TARGETS=		# blank


.include "../../mk/ocaml.mk"
.include "../../mk/bsd.prefs.mk"

# .include "options.mk"

# EGDIR=		${PREFIX}/share/coq/examples
# CONF_FILES=	${EGDIR}/coqide-gtk2rc ${PKG_SYSCONFDIR}/xdg/coq/coqide-gtk2rc

.include "../../math/ocaml-zarith/buildlink3.mk"
.include "../../mk/pthread.buildlink3.mk"
.include "../../mk/bsd.pkg.mk"

---8<---

The contents of accompanying patches have been:


---8<---


$NetBSD$

--- Makefile.make.orig	2021-01-07 07:53:41.000000000 +0000
+++ Makefile.make
@@ -48,7 +48,7 @@
 # !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt         !!
 # "-not -name ." to avoid skipping everything since we "find ."
 # "-type d" to be able to find .merlin.in files
-FIND_SKIP_DIRS:=-not -name . '(' \
+FIND_SKIP_DIRS:=\! -name . '(' \
   -name '{arch}' -o \
   -name '.*' -type d -o \
   -name '_darcs' -o \

$NetBSD$

--- configure.ml.orig	2021-01-07 07:53:41.000000000 +0000
+++ configure.ml
@@ -191,7 +191,12 @@ let which prog =
     | dir :: path ->
       let file = if os_type_win32 then dir/prog^".exe" else dir/prog in
       if is_executable file then file else search path
-  in search global_path
+  in
+  if Filename.is_relative prog then
+    search global_path
+  else
+    if is_executable prog then prog
+    else raise Not_found
 
 let program_in_path prog =
   try let _ = which prog in true with Not_found -> false
@@ -830,14 +835,14 @@ let strip =
 (** * Documentation : do we have latex, hevea, ... *)
 
 let check_sphinx_deps () =
-  ignore (run (which "python3") ["doc/tools/coqrst/checkdeps.py"])
+  ignore (run (which "@@PYTHON@@") ["doc/tools/coqrst/checkdeps.py"])
 
 let check_doc () =
   let err s =
     die (sprintf "A documentation build was requested, but %s was not found." s);
   in
-  if not (program_in_path "python3") then err "python3";
-  if not (program_in_path "sphinx-build") then err "sphinx-build";
+  if not (program_in_path "@@PYTHON@@") then err "@@PYTHON@@";
+  if not (program_in_path "@@SPHINX_BUILD@@") then err "@@SPHINX_BUILD@@";
   check_sphinx_deps ()
 
 let _ = if !prefs.withdoc then check_doc ()


$NetBSD$

--- dev/doc/build-system.dev.txt.orig	2021-02-07 23:44:01.786032460 +0000
+++ dev/doc/build-system.dev.txt
@@ -112,11 +112,11 @@ The recommended style of using FIND_SKIP
 The parentheses even in the one-criteria case is so that if one adds
 other conditions, e.g. change the first example to the second
 
- find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print
+ find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and \! -name '*.bak.example' ')' -print
 
 one is not tempted to write
 
- find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print
+ find . $(FIND_SKIP_DIRS) -name '*.example' -and \! -name '*.bak.example' -print
 
 because this will not necessarily work as expected; $(FIND_SKIP_DIRS)
 ends with an -or, and how it combines with what comes later depends on


$NetBSD$

--- doc/dune.orig	2021-01-07 07:53:41.000000000 +0000
+++ doc/dune
@@ -32,7 +32,7 @@
   unreleased.rst
   (env_var SPHINXWARNOPT))
  (action
-  (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
+  (run env COQLIB=%{project_root} @@SPHINX_BUILD@@ -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
 
 (rule
  (targets refman-pdf)
@@ -48,7 +48,7 @@
   (env_var SPHINXWARNOPT))
  (action
   (progn
-   (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
+   (run env COQLIB=%{project_root} @@SPHINX_BUILD@@ -q %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
    (chdir %{targets} (run make LATEXMKOPTS=-silent)))))
 
 ; Installable directories are not yet fully supported by Dune.  See


$NetBSD$

--- test-suite/coq-makefile/template/init.sh.orig	2021-02-07 23:43:12.385871354 +0000
+++ test-suite/coq-makefile/template/init.sh
@@ -3,7 +3,7 @@
 
 rm -rf _test
 mkdir _test
-find . -maxdepth 1 -not -name . -not -name _test -exec cp -r '{}' -t _test ';'
+find . -maxdepth 1 \! -name . \! -name _test -exec cp -r '{}' -t _test ';'
 
 cd _test || exit 1
 mkdir -p src


$NetBSD$

--- test-suite/report.sh.orig	2021-02-07 23:42:10.826888274 +0000
+++ test-suite/report.sh
@@ -22,7 +22,7 @@ rm "$FAILED"
 
 # print info
 if [ -n "$CI" ] || [ -n "$PRINT_LOGS" ]; then
-    find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do
+    find logs/ -name '*.log' \! -name 'summary.log' -print0 | while IFS= read -r -d '' file; do
         printf '%s\n' "$file"
         cat "$file"
         printf '\n'

---8<---

(note: some of these patches were sent upstream; cf. https://github.com/coq/coq/issues/13845)

Unfortunately, at this point, I see the following outcome.  The build of coqtop binary through pkgsrc takes much longer than through the opam, and appears to use much more RAM (up to 100Gb).  Furthermore, the test scripts takes around 30 to 80 seconds to execute when it is fed to to the coqtop binary resulting from this build.

I have reasons to believe that these build issues could be resolved to satisfaction -- after all there's a successful opam-based build -- and that would lead to integration newer release of coq into pkgsrc, and also of the dune build system for this package.  I would appreciate further advice as I seek the solution to this issue.

>How-To-Repeat:
N/A
>Fix:
N/A
Prev by Date: Re: pkg/55989: archivers/zstd depends on coreutils
Next by Date: Re: pkg/55988: lang/coq: request to update to dune build system and latest release
Previous by Thread: Re: pkg/55989 (archivers/zstd depends on coreutils)
Next by Thread: Re: pkg/55988: lang/coq: request to update to dune build system and latest release
Indexes:
Home | Main Index | Thread Index | Old Index