Commit 76bf7fcf authored by Robbert Krebbers's avatar Robbert Krebbers

Move to solutions folder and update Makefile.

parent 7b5001ea
EXTRA_DIR:=coqdocjs/extra
COQDOCFLAGS:= \
--toc --toc-depth 2 --html --interpolate \
--index indexpage --no-lib-name --parse-comments \
--with-header $(EXTRA_DIR)/header.html --with-footer $(EXTRA_DIR)/footer.html
export COQDOCFLAGS
# Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony
+@make -f Makefile.coq $@
all: Makefile.coq
+@make -f Makefile.coq all
html: Makefile.coq phony
rm -fr html
@$(MAKE) -f Makefile.coq html
cp $(EXTRA_DIR)/resources/* html
.PHONY: all html
.PHONY: all
clean: Makefile.coq
+@make -f Makefile.coq clean
find theories tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
find solutions tests \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
rm -f Makefile.coq .lia.cache
.PHONY: clean
......@@ -42,14 +29,8 @@ build-dep: build-dep/opam phony
@# 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 "# Pinning build-dep package." && \
if opam --version | grep "^1\." -q; then \
BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
else \
opam install $(OPAMFLAGS) build-dep/; \
fi
@echo "# Installing build-dep package."
@opam install $(OPAMFLAGS) build-dep/
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ;
......
-Q theories tutorial_popl20
-Q solutions tutorial_popl20
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
......@@ -8,19 +8,19 @@
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
theories/language.v
theories/polymorphism.v
theories/types.v
theories/typed.v
theories/sem_types.v
theories/sem_type_formers.v
theories/sem_typed.v
theories/sem_operators.v
theories/compatibility.v
theories/fundamental.v
theories/safety.v
theories/two_state_ghost.v
theories/symbol_ghost.v
theories/unsafe.v
theories/parametricity.v
theories/interp.v
solutions/language.v
solutions/polymorphism.v
solutions/types.v
solutions/typed.v
solutions/sem_types.v
solutions/sem_type_formers.v
solutions/sem_typed.v
solutions/sem_operators.v
solutions/compatibility.v
solutions/fundamental.v
solutions/safety.v
solutions/two_state_ghost.v
solutions/symbol_ghost.v
solutions/unsafe.v
solutions/parametricity.v
solutions/interp.v
......@@ -354,7 +354,7 @@ Qed.
(** ** Exercise (not_typed, easy) *)
(** Prove that the programs [unsafe_pure] and [unsafe_ref] from [language.v]
cannot be typed using the syntactic type system. *)
Lemma unsafe_pure_not_typed Γ τ : ¬ (Γ unsafe_pure : τ).
Lemma unsafe_pure_not_typed τ : ¬ ( unsafe_pure : τ).
(* REMOVE *) Proof.
intros Htyped.
repeat
......@@ -364,7 +364,7 @@ Lemma unsafe_pure_not_typed Γ τ : ¬ (Γ ⊢ᵥ unsafe_pure : τ).
end.
Qed.
Lemma unsafe_ref_not_typed Γ τ : ¬ (Γ unsafe_ref : τ).
Lemma unsafe_ref_not_typed τ : ¬ ( unsafe_ref : τ).
(* REMOVE *) Proof.
intros Htyped.
repeat
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment