diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b0637ccd850..a64027400da 100644 --- a/.github/workflows/ci.yml +++ b/.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: diff --git a/contrib/HoTTBook.v b/contrib/HoTTBook.v index adda0e5c78b..3b50dd04953 100644 --- a/contrib/HoTTBook.v +++ b/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 diff --git a/contrib/HoTTBookExercises.v b/contrib/HoTTBookExercises.v index b9be4685730..bd6ecdf2c89 100644 --- a/contrib/HoTTBookExercises.v +++ b/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. diff --git a/contrib/dune b/contrib/dune new file mode 100644 index 00000000000..9d5259333e0 --- /dev/null +++ b/contrib/dune @@ -0,0 +1,6 @@ +(coq.theory + (name HoTT.Contrib) + (package coq-hott) + (flags -noinit -indices-matter -color on) + (theories HoTT)) + diff --git a/hott.opam b/coq-hott.opam similarity index 59% rename from hott.opam rename to coq-hott.opam index 871a81e3da2..3f9cdcff49d 100644 --- a/hott.opam +++ b/coq-hott.opam @@ -1,17 +1,5 @@ +# This file is generated by dune, edit dune-project instead opam-version: "2.0" -maintainer: [ "Jason Gross " "Ali Caglayan " ] -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 " "Ali Caglayan " +] +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" diff --git a/dune b/dune new file mode 100644 index 00000000000..1e26d751e30 --- /dev/null +++ b/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))) diff --git a/dune-project b/dune-project new file mode 100644 index 00000000000..2a80c28e742 --- /dev/null +++ b/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 " + "Ali Caglayan ") + +(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)))) diff --git a/etc/generate_coqproject.sh b/etc/generate_coqproject.sh old mode 100644 new mode 100755 index 417dedb70e2..21ba19b3991 --- a/etc/generate_coqproject.sh +++ b/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" diff --git a/theories/dune b/theories/dune new file mode 100644 index 00000000000..e033640db0a --- /dev/null +++ b/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