parent
38a2cffd4c
commit
08e64224e9
@ -0,0 +1,20 @@
|
|||||||
|
*.vo
|
||||||
|
*.vos
|
||||||
|
*.vok
|
||||||
|
*.vio
|
||||||
|
*.glob
|
||||||
|
*.cache
|
||||||
|
*.aux
|
||||||
|
\#*\#
|
||||||
|
.\#*
|
||||||
|
*~
|
||||||
|
*.bak
|
||||||
|
Makefile.coq
|
||||||
|
Makefile.coq.conf
|
||||||
|
.Makefile.coq.d
|
||||||
|
.coq-native/
|
||||||
|
builddep
|
||||||
|
_opam
|
||||||
|
tags
|
||||||
|
_build
|
||||||
|
public
|
@ -0,0 +1,55 @@
|
|||||||
|
# Default target
|
||||||
|
all: Makefile.coq
|
||||||
|
+@$(MAKE) -f Makefile.coq all
|
||||||
|
.PHONY: all
|
||||||
|
|
||||||
|
# Permit local customization
|
||||||
|
-include Makefile.local
|
||||||
|
|
||||||
|
# Forward most targets to Coq makefile (with some trick to make this phony)
|
||||||
|
%: Makefile.coq phony
|
||||||
|
@#echo "Forwarding $@"
|
||||||
|
+@$(MAKE) -f Makefile.coq $@
|
||||||
|
phony: ;
|
||||||
|
.PHONY: phony
|
||||||
|
|
||||||
|
clean: Makefile.coq
|
||||||
|
+@$(MAKE) -f Makefile.coq clean
|
||||||
|
@# Make sure not to enter the `_opam` folder.
|
||||||
|
find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
|
||||||
|
rm -f Makefile.coq .lia.cache builddep/*
|
||||||
|
.PHONY: clean
|
||||||
|
|
||||||
|
# Create Coq Makefile.
|
||||||
|
Makefile.coq: _CoqProject Makefile
|
||||||
|
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
|
||||||
|
|
||||||
|
# Install build-dependencies
|
||||||
|
OPAMFILES=$(wildcard *.opam)
|
||||||
|
BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
|
||||||
|
|
||||||
|
builddep/%-builddep.opam: %.opam Makefile
|
||||||
|
@echo "# Creating builddep package for $<."
|
||||||
|
@mkdir -p builddep
|
||||||
|
@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
|
||||||
|
|
||||||
|
builddep-opamfiles: $(BUILDDEPFILES)
|
||||||
|
.PHONY: builddep-opamfiles
|
||||||
|
|
||||||
|
builddep: builddep-opamfiles
|
||||||
|
@# We want opam to not just install the build-deps now, but to also keep satisfying these
|
||||||
|
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions
|
||||||
|
@# that are incompatible with our build requirements.
|
||||||
|
@# To achieve this, we create a fake opam package that has our build-dependencies as
|
||||||
|
@# dependencies, but does not actually install anything itself.
|
||||||
|
@echo "# Installing builddep packages."
|
||||||
|
@opam install $(OPAMFLAGS) -y $(BUILDDEPFILES)
|
||||||
|
.PHONY: builddep
|
||||||
|
|
||||||
|
# Backwards compatibility target
|
||||||
|
build-dep: builddep
|
||||||
|
.PHONY: build-dep
|
||||||
|
|
||||||
|
# Some files that do *not* need to be forwarded to Makefile.coq.
|
||||||
|
# ("::" lets Makefile.local overwrite this.)
|
||||||
|
Makefile Makefile.local _CoqProject $(OPAMFILES):: ;
|
@ -0,0 +1,19 @@
|
|||||||
|
opam-version: "2.0"
|
||||||
|
name: "coq-semantics-course"
|
||||||
|
license: "BSD-3-Clause"
|
||||||
|
maintainer: "Simon Spies, Lennard Gäher"
|
||||||
|
authors: "Derek Dreyer, Simon Spies, Lennard Gäher"
|
||||||
|
synopsis: "Best course this side of the milky way"
|
||||||
|
homepage: "https://plv.mpi-sws.org/semantics-course/"
|
||||||
|
bug-reports: "https://gitlab.mpi-sws.org/FP/semantics-course/issues"
|
||||||
|
version: "dev"
|
||||||
|
|
||||||
|
depends: [
|
||||||
|
"coq" { (>= "8.18" & < "8.19~") | (= "dev") }
|
||||||
|
"coq-iris-heap-lang" { (= "4.1.0") | (= "dev") }
|
||||||
|
"coq-equations" { (= "1.3+8.18") }
|
||||||
|
"coq-autosubst" { (= "1.8") | (= "dev") }
|
||||||
|
]
|
||||||
|
|
||||||
|
build: [make "-j%{jobs}%"]
|
||||||
|
install: [make "install"]
|
Loading…
Reference in new issue