diff options
| -rw-r--r-- | .github/CODEOWNERS | 2 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 8 | ||||
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | Makefile.doc | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-plugin_tutorial.sh | 12 | ||||
| -rw-r--r-- | doc/plugin_tutorial/Makefile | 21 | ||||
| -rw-r--r-- | doc/plugin_tutorial/tuto3/theories/Data.v | 11 |
10 files changed, 50 insertions, 28 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index b0e79fb1b2..2a641263e3 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -71,6 +71,8 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes +/doc/plugin_tutorial/ @ybertot + ########## Coqchk ########## /checker/ @ppedrot diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f54f64bf28..d9ae36af8c 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -544,8 +544,12 @@ plugin:ci-mtac2: plugin:ci-paramcoq: <<: *ci-template -plugin:ci-plugin_tutorial: - <<: *ci-template +plugin:plugin-tutorial: + stage: test + dependencies: [] + script: + - ./configure -local -warn-error yes + - make -j "$NJOBS" plugin-tutorial plugin:ci-quickchick: <<: *ci-template-flambda @@ -61,7 +61,8 @@ FIND_SKIP_DIRS:='(' \ -name 'user-contrib' -o \ -name 'test-suite' -o \ -name '.opamcache' -o \ - -name '.coq-native' \ + -name '.coq-native' -o \ + -name 'plugin_tutorial' \ ')' -prune -o define find @@ -191,7 +192,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean plugin-tutorialclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean gramlibclean @@ -237,7 +238,7 @@ docclean: rm -f doc/coq.tex rm -rf doc/sphinx/_build -archclean: clean-ide optclean voclean +archclean: clean-ide optclean voclean plugin-tutorialclean rm -rf _build rm -f $(ALLSTDLIB).* @@ -278,6 +279,9 @@ timingclean: -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + +plugin-tutorialclean: + +$(MAKE) -C $(PLUGINTUTO) clean + # Ensure that every compiled file around has a known source file. # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. diff --git a/Makefile.ci b/Makefile.ci index 84be169f57..b8bff98f5f 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -36,7 +36,6 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-plugin_tutorial \ ci-quickchick \ ci-relation-algebra \ ci-sf \ diff --git a/Makefile.common b/Makefile.common index 9f7ed9d46e..2dced04967 100644 --- a/Makefile.common +++ b/Makefile.common @@ -168,6 +168,8 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx) ALLSTDLIB := test-suite/misc/universes/all_stdlib +PLUGINTUTO := doc/plugin_tutorial + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.doc b/Makefile.doc index 9e6ec4955a..48cdcebddb 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -89,6 +89,10 @@ stdlib: \ full-stdlib: \ doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf +.PHONY: plugin-tutorial +plugin-tutorial: states tools + +$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO) + ###################################################################### ### Implicit rules ###################################################################### diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e74a7853b9..e38a866f56 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -233,13 +233,6 @@ : "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" ######################################################################## -# plugin_tutorial -######################################################################## -: "${plugin_tutorial_CI_REF:=master}" -: "${plugin_tutorial_CI_GITURL:=https://github.com/ybertot/plugin_tutorials}" -: "${plugin_tutorial_CI_ARCHIVEURL:=${plugin_tutorial_CI_GITURL}/archive}" - -######################################################################## # menhirlib ######################################################################## : "${menhirlib_CI_REF:=master}" diff --git a/dev/ci/ci-plugin_tutorial.sh b/dev/ci/ci-plugin_tutorial.sh deleted file mode 100755 index 6c26a71a21..0000000000 --- a/dev/ci/ci-plugin_tutorial.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download plugin_tutorial - -( cd "${CI_BUILD_DIR}/plugin_tutorial" && \ - pushd tuto0 && make && popd && \ - pushd tuto1 && make && popd && \ - pushd tuto2 && make && popd && \ - pushd tuto3 && make && popd ) diff --git a/doc/plugin_tutorial/Makefile b/doc/plugin_tutorial/Makefile new file mode 100644 index 0000000000..7f1833fadd --- /dev/null +++ b/doc/plugin_tutorial/Makefile @@ -0,0 +1,21 @@ + +TUTOS:= \ + tuto0 \ + tuto1 \ + tuto2 \ + tuto3 + +all: $(TUTOS) + +.PHONY: $(TUTOS) all + +$(TUTOS): %: + +$(MAKE) -C $@ + +CLEANS:=$(addsuffix -clean, $(TUTOS)) +.PHONY: clean $(CLEANS) + +clean: $(CLEANS) + +%-clean: + +$(MAKE) -C $* clean diff --git a/doc/plugin_tutorial/tuto3/theories/Data.v b/doc/plugin_tutorial/tuto3/theories/Data.v index 0b07fee4f2..f7395d686b 100644 --- a/doc/plugin_tutorial/tuto3/theories/Data.v +++ b/doc/plugin_tutorial/tuto3/theories/Data.v @@ -1,4 +1,4 @@ -Require Import ArithRing. + Inductive pack (A: Type) : Type := packer : A -> pack A. @@ -18,7 +18,11 @@ Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}. Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}. Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n). -Proof. intros H; ring [H]. Qed. +Proof. + intros []. + simpl. rewrite <-plus_n_O, <-plus_n_Sm. + reflexivity. +Qed. Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) := {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}. @@ -51,7 +55,8 @@ Canonical Structure can_ev0 : S_ev 0 := Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n). Proof. intros s; exists (S (S (double_of _ s))). -destruct s as [a P]. simpl. ring [P]. +destruct s as [a P]. +exact (even_rec _ _ P). Defined. Canonical Structure can_ev_rec. |