Dune support (HoTT#1687)

<!-- ps-id: 954ea380-2db6-46f1-b33c-6f3384074297 -->

Signed-off-by: Ali Caglayan <alizter@gmail.com>

.github/workflows/ci.yml

@@ -50,9 +50,12 @@ jobs:
     - name: Build HoTT
       uses: coq-community/docker-coq-action@v1
       with:
-        opam_file: 'hott.opam'
+        opam_file: 'coq-hott.opam'
         coq_version: ${{ env.coq-version }}
         ocaml_version: ${{ env.ocaml-version }}
+        export: 'OPAMWITHTEST'
+      env:
+        OPAMWITHTEST: 'true'
 
   # Quick build
   quick-build:

contrib/HoTTBook.v

@@ -57,9 +57,12 @@
 
 *)
 
-Require Import HoTT.
-Require Import HoTT.Metatheory.Core HoTT.Metatheory.IntervalImpliesFunext HoTT.Metatheory.UnivalenceImpliesFunext.
-Require HoTT.Categories.
+From HoTT Require Import HoTT.
+From HoTT Require Categories.
+From HoTT Require Import
+  Metatheory.Core
+  Metatheory.IntervalImpliesFunext
+  Metatheory.UnivalenceImpliesFunext.
 From HoTT.Classes Require
   interfaces.abstract_algebra
   interfaces.orders

contrib/HoTTBookExercises.v

@@ -23,9 +23,12 @@
 
 *)
 
-Require Import HoTT.
-Require Import Spaces.Nat.
-Require Import HoTT.Metatheory.Core HoTT.Metatheory.FunextVarieties HoTT.Metatheory.UnivalenceImpliesFunext.
+From HoTT Require Import HoTT.
+From HoTT Require Import Spaces.Nat.
+From HoTT Require Import
+  Metatheory.Core
+  Metatheory.FunextVarieties
+  Metatheory.UnivalenceImpliesFunext.
 
 Local Open Scope nat_scope.
 Local Open Scope type_scope.

contrib/dune

@@ -0,0 +1,6 @@
+(coq.theory
+ (name HoTT.Contrib)
+ (package coq-hott)
+ (flags -noinit -indices-matter -color on)
+ (theories HoTT))
+

hott.opam → coq-hott.opam

@@ -1,17 +1,5 @@
+# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-maintainer: [ "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>" ]
-homepage: "http://homotopytypetheory.org/"
-bug-reports: "https://github.com/HoTT/HoTT/issues"
-license: "BSD-2-Clause"
-build: [
-  [make "-j%{jobs}%"]
-]
-install: [make "install"]
-depends: [
-  "coq" {>= "8.16~"}
-]
-authors: ["The HoTT Library Development Team"]
-dev-repo: "git+https://github.com/HoTT/HoTT.git"
 synopsis: "The Homotopy Type Theory library"
 description: """
 To use the HoTT library, the following flags must be passed to coqc:
@@ -20,7 +8,30 @@ To use the HoTT library in a project, add the following to _CoqProject:
   -arg -noinit
   -arg -indices-matter
 """
-tags: [ "logpath:HoTT" ]
-url {
-  src: "git+https://github.com/HoTT/HoTT.git#master"
-}
+maintainer: [
+  "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>"
+]
+authors: ["The HoTT Library Development Team"]
+license: "BSD-2-Clause"
+homepage: "http://homotopytypetheory.org/"
+bug-reports: "https://github.com/HoTT/HoTT/issues"
+depends: [
+  "dune" {>= "3.5"}
+  "coq" {>= "8.16.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/HoTT/HoTT.git"

dune

@@ -0,0 +1,26 @@
+; Rule for generating coq_project
+; This uses (mode promote) in order to put _CoqProject in the source tree.
+; This isn't actually needed for dune but is useful when working with editors.
+
+(rule
+ (target _CoqProject)
+ (deps
+  ./etc/generate_coqproject.sh
+  (source_tree theories)
+  (source_tree contrib))
+ (mode promote)
+ (package coq-hott)
+ (action
+  (setenv
+   GENERATE_COQPROJECT_FOR_DUNE
+   true
+   (bash ./etc/generate_coqproject.sh))))
+
+; Rule for validation: dune build @runtest
+
+(rule
+ (alias runtest)
+ (deps
+  (glob_files_rec ./*.vo))
+ (action
+  (run coqchk -R ./theories HoTT -Q contrib HoTT.Contrib %{deps} -o)))

dune-project

@@ -0,0 +1,28 @@
+(lang dune 3.5)
+
+(using coq 0.6)
+
+(name coq-hott)
+
+(generate_opam_files true)
+
+(source
+ (github HoTT/HoTT))
+
+(homepage "http://homotopytypetheory.org/")
+
+(license BSD-2-Clause)
+
+(authors "The HoTT Library Development Team")
+
+(maintainers
+ "Jason Gross <jgross@mit.edu>"
+ "Ali Caglayan <alizter@gmail.com>")
+
+(package
+ (name coq-hott)
+ (synopsis "The Homotopy Type Theory library")
+ (description
+  "To use the HoTT library, the following flags must be passed to coqc:\n  -noinit -indices-matter\nTo use the HoTT library in a project, add the following to _CoqProject:\n  -arg -noinit\n  -arg -indices-matter\n")
+ (depends
+  (coq (>= 8.16.0))))

etc/generate_coqproject.sh

@@ -23,11 +23,20 @@ COQPROJECT_HEADER=\
 ###############################################################################
 -R theories HoTT
 -Q contrib HoTT.Contrib
+
 -arg -noinit
 -arg -indices-matter
 -arg -native-compiler -arg no
 "
 
+if [ "$GENERATE_COQPROJECT_FOR_DUNE" == "true" ]; then
+  COQPROJECT_HEADER="$COQPROJECT_HEADER
+# Dune compatbility 
+-R _build/default/theories HoTT
+-Q _build/default/contrib HoTT.Contrib
+"
+fi
+
 ## Generate _CoqProject
 printf -v NEW_COQPROJECT '%s\n%s' "$COQPROJECT_HEADER" "$SORTED_V_FILES"
 

theories/dune

@@ -0,0 +1,14 @@
+; Tell dune to look through subdirectories
+
+(include_subdirs qualified)
+
+; Main theory stanza telling dune how the HoTT library is compiled
+
+(coq.theory
+ (name HoTT)
+ (package coq-hott)
+ (modules :standard)
+ (flags -noinit -indices-matter -color on))
+
+; TODO: Tests
+; Prob need to move tests into tests folder