Commit ee88f0b6 authored by Michael Sammler's avatar Michael Sammler
Browse files

add simpl.v

parent 7b391b72
*.v gitlab-language=coq
# Convert to native line endings on checkout.
*.ref text
# Shell scripts need Linux line endings.
*.sh eol=lf
*.vo
*.vos
*.vok
*.vio
*.v.d
.coqdeps.d
*.glob
*.cache
*.aux
\#*\#
.\#*
*~
*.bak
.coqdeps.d
.coq-native/
*.crashcoqide
.env
builddep/
_CoqProject.*
Makefile.coq
Makefile.coq.conf
.Makefile.coq.d
Makefile.package.*
.Makefile.package.*
# 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) $(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):: ;
# Coq Tricks
This repository contain a collection of interesting tricks and facts about Coq that were useful during the development of Iris.
- [simpl.v](theories/simpl.v): `simpl` and similar reduction insert casts even if they do not change the goal which can slow down Qed.
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
# Search paths for all packages. They must all match the regex
-Q theories tricks
theories/simpl.v
\ No newline at end of file
(** [simpl] and other reduction tactics inserts casts in the goal even
if they don't change the goal. This can lead to a slower Coq. To avoid
this behaviour, one can use [try progress simpl] instead of [simpl].
See also the discussion at
https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/exact_no_check.2C.20repeated.20casts.20in.20proof.20terms
and https://github.com/coq/coq/pull/15104 *)
Goal 1 = 1.
Set Printing All.
Show Proof.
(** => ?Goal *)
simpl.
Show Proof.
(** => (?Goal : @eq nat (S O) (S O))
Notice the cast. *)
Undo.
Show Proof.
(** => ?Goal *)
try progress simpl.
Show Proof.
(** => ?Goal.
Notice that there is no cast *)
Abort.
Supports Markdown
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