Use alectryon to generate doc with proof state

Let's use this awesome tool: https://github.com/cpitclaudel/alectryon

While at it, also update the CI configuration to minimize the jobs that run in wip- branches.

.gitlab-ci.yml

+###################### Global Config ######################
+
 workflow:
   rules:
     - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
@@ -9,6 +11,12 @@ stages:
   - build
   - process
 
+###################### Rules and Scripts ##################
+
+.not_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
+
 .build-common:
   stage: build
   script:
@@ -70,17 +78,40 @@ stages:
     - "*/*/*/*/*/*/*/*/*/*.glob"
     expire_in: 1 week
 
+.doc: 
+  extends:
+    - .preferred-stable-version
+  stage: process
+  script:
+    - make html -j ${NJOBS}
+    - mv html with-proofs
+    - make gallinahtml -j ${NJOBS}
+    - mv html without-proofs
+    - make htmlpretty -j ${NJOBS}
+    - mv html pretty
+
+
+###################### The Jobs ######################
+
 1.10.0-coq-8.11:
-  extends: .build
+  extends:
+    - .build
+    - .not_in_wip_branches
 
 1.11.0-coq-8.11:
-  extends: .build
+  extends:
+    - .build
+    - .not_in_wip_branches
 
 1.11.0-coq-8.12:
-  extends: .build
+  extends:
+    - .build
+    - .not_in_wip_branches
 
 1.12.0-coq-8.13:
-  extends: .build
+  extends:
+    - .build
+    - .not_in_wip_branches
 
 build-for-process:
   extends:
@@ -88,9 +119,8 @@ build-for-process:
     - .collect-vo-files
 
 build-for-process-classic:
-  rules:
-    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
   extends:
+    - .not_in_wip_branches
     - .build-for-process-classic
     - .collect-vo-files
 
@@ -101,27 +131,32 @@ proof-length:
     - scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
 
 spell-check:
+  extends:  
+    - .not_in_wip_branches  
   stage: build
   image: bbbrandenburg/aspell-ci
   script:
     - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
 
+# mathcomp-dev with stable Coq 8.13
 coq-8.13:
   extends:
     - .build-dev
+    - .not_in_wip_branches    
   # it's ok to fail with an unreleased version of ssreflect
   allow_failure: true
 
+# mathcomp-dev with coq-dev
 coq-dev:
   extends:
     - .build-dev
+    - .not_in_wip_branches    
   # it's ok to fail with an unreleased version of ssreflect and Coq
   allow_failure: true
 
 validate:
-  rules:
-    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
   extends:
+    - .not_in_wip_branches
     - .preferred-stable-version
   stage: process
   needs: ["build-for-process"]
@@ -130,9 +165,8 @@ validate:
   script: make validate
 
 validate-classic:
-  rules:
-    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
   extends:
+    - .not_in_wip_branches  
     - .preferred-stable-version
   stage: process
   needs: ["build-for-process-classic"]
@@ -140,18 +174,6 @@ validate-classic:
     - build-for-process-classic
   script: make validate
 
-.doc: 
-  extends:
-    - .preferred-stable-version
-  stage: process
-  script:
-    - make html -j ${NJOBS}
-    - mv html with-proofs
-    - make gallinahtml -j ${NJOBS}
-    - mv html without-proofs
-    - make htmlpretty -j ${NJOBS}
-    - mv html pretty
-
 doc:
   extends:
     - .doc
@@ -167,9 +189,8 @@ doc:
     expire_in: 1 week
 
 doc-classic:
-  rules:
-    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
   extends:
+    - .not_in_wip_branches  
     - .doc
   needs: ["build-for-process-classic"]
   dependencies:
@@ -183,9 +204,8 @@ doc-classic:
     expire_in: 1 week
 
 proof-state:
-  rules:
-    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
   extends:
+    - .not_in_wip_branches  
     - .preferred-stable-version
   stage: process
   needs: ["build-for-process"]