Merge pull request #41 from rocq-community/fix-link-check

Fix markdown link check

Author: tchajed

.github/workflows/check-links.yml

@@ -16,4 +16,4 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Check for broken Markdown links
-        uses: gaurav-nelson/github-action-markdown-link-check@v1
+        uses: tcort/github-action-markdown-link-check@v1

README.md

@@ -75,7 +75,7 @@ To build all the examples in `src/`, run `make`.
   - `in * |- *` (everywhere, same as `in *`)
     These forms would be especially useful if occurrence clauses were first-class objects; that is, if tactics could take and pass occurrence clauses. Currently user-defined tactics support occurrence clauses via a set of tactic notations.
 - Defining tactics (`Tactic Notation`s) that accept multiple optional parameters directly is cumbersome, but it can be done more flexibly using Ltac2. An example can be found in [TacticNotationOptionalParams.v](src/TacticNotationOptionalParams.v).
-- You can use notations to shorten repetitive Ltac patterns (much like Haskell's [PatternSynonyms](https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms#Motivatingexample)). Define a notation with holes (underscores) and use it in an Ltac match, eg `Notation anyplus := (_ + _).` and then
+- You can use notations to shorten repetitive Ltac patterns (much like Haskell's [PatternSynonyms](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html)). Define a notation with holes (underscores) and use it in an Ltac match, eg `Notation anyplus := (_ + _).` and then
   ```coq
   match goal with
   | |- context[anyplus] => idtac
@@ -97,7 +97,7 @@ To build all the examples in `src/`, run `make`.
 - If you need to apply a theorem to a hypothesis and then immediately destruct the result, there's a concise way to do it without repetition: `apply thm in H as [x H]`, for example, might be used then `thm` produces an existential for a variable named `x`.
 - If you have a hypothesis `H: a = b` and need `f a = f b`, you can use `apply (f_equal f) in H`. (Strictly speaking this is just using the `f_equal` theorem in the standard library, but it's also very much like the inverse direction for the `f_equal` tactic.)
 - If you want to both run Ltac and return a `constr`, you can do so by wrapping the side effect in `let _ := match goal with _ => side_effect_tactic end in ...`. See <https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884> for Jason Gross's much more thorough explanation.
-- If you want `lia` to help with non-linear arithmetic involving division or modulo (or the similar `quot` and `rem`), you can do that for simple cases with `Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.` See [DivMod.v](src/DivMod.v) for an example and the [micromega documentation](https://coq.github.io/doc/master/refman/addendum/micromega.html) the full details.
+- If you want `lia` to help with non-linear arithmetic involving division or modulo (or the similar `quot` and `rem`), you can do that for simple cases with `Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.` See [DivMod.v](src/DivMod.v) for an example and the [micromega documentation](https://rocq-prover.org/doc/master/refman/addendum/micromega.html) the full details.
 - Coq's `admit` will force you to use `Admitted`. If you want to use Qed, you can instead use `Axiom falso : False. Ltac admit := destruct falso.` This can be useful for debugging Qed errors (say, due to universes) or slow Qeds.
 
 ## Gallina
@@ -140,7 +140,7 @@ To build all the examples in `src/`, run `make`.
   see some simple examples of using it in [Modules.v](src/Modules.v). In user
   code, I've found module types and module functors to be more trouble than they're worth 90% of the time - the biggest issue is that once something is in a module type, the only way to extend it is with a new module that wraps an existing module, and the only way to use the extension is to instantiate it. At the same time, you can mostly simulate module types with records.
 - Coq type class resolution is extremely flexible. There's a hint database called `typeclass_instances` and typeclass resolution is essentially `eauto with typeclass_instances`. Normally you add to this database with commands like `Instance`, but you can add whatever you want to it, including `Hint Extern`s. See [coq-record-update](https://github.com/tchajed/coq-record-update) for a practical example.
-- Classes are a bit special compared to any other type. First of all, in `(_ : T x1 x2)` Coq will only trigger type class resolution to fill the hole when `T` is a class. Second, classes get special implicit generalization behavior; specifically, you can write `{T}` and Coq will automatically generalize the _arguments to T_, which you don't even have to write down. See [the manual on implicit generalization](https://coq.github.io/doc/master/refman/language/gallina-extensions.html#implicit-generalization) for more details. Note that you don't have to use `Class` at declaration time to make something a class; you can do it after the fact with `Existing Class T`.
+- Classes are a bit special compared to any other type. First of all, in `(_ : T x1 x2)` Coq will only trigger type class resolution to fill the hole when `T` is a class. Second, classes get special implicit generalization behavior; specifically, you can write `{T}` and Coq will automatically generalize the _arguments to T_, which you don't even have to write down. See [the manual on implicit generalization](https://rocq-prover.org/doc/master/refman/language/extensions/implicit-arguments.html#implicit-generalization) for more details. Note that you don't have to use `Class` at declaration time to make something a class; you can do it after the fact with `Existing Class T`.
 - `Set Printing Projections` is nice in theory if you use records, but it
   interacts poorly with classes. See [Projections.v](src/Projections.v).
 
@@ -151,7 +151,7 @@ To build all the examples in `src/`, run `make`.
 - `Locate` can search for notation, including partial searches.
 - `Optimize Heap` (undocumented) runs GC (specifically [`Gc.compact`](https://ocaml.org/manual/5.2/api/Gc.html#VALcompact))
 - `Optimize Proof` (undocumented) runs several simplifications on the current proof term (see [`Proofview.compact`](https://github.com/coq/coq/blob/9a4ca53a3a021cb16de7706ec79a26e49f54de49/engine/proofview.ml#L40))
-- (in Coq 8.12 and earlier) `Generalizable Variable A` enables implicit generalization; `` Definition id `(x:A) := x `` will implicitly add a parameter `A` before `x`. `Generalizable All Variables` enables implicit generalization for any identifier. Note that this surprisingly allows generalization without a backtick in Instances. [Issue #6030](https://github.com/coq/coq/issues/6030) generously requests this behavior be documented, but it should probably require enabling some option. This has been fixed in Coq 8.13; the old behavior requires `Set Instance Generalized Output`. In Coq 8.14 the option has been removed.
+- (in Coq 8.12 and earlier) `Generalizable Variable A` enables implicit generalization; `` Definition id `(x:A) := x `` will implicitly add a parameter `A` before `x`. `Generalizable All Variables` enables implicit generalization for any identifier. Note that this surprisingly allows generalization without a backtick in Instances. [Issue #6030](https://github.com/rocq-prover/rocq/issues/6030) generously requests this behavior be documented, but it should probably require enabling some option. This has been fixed in Coq 8.13; the old behavior requires `Set Instance Generalized Output`. In Coq 8.14 the option has been removed.
 - `Check` supports partial terms, printing a type along with a context of evars. A cool example is `Check (id _ _)`, where the first underscore must be a function (along with other constraints on the types involved).
 - The above also works with named existentials. For example, `Check ?[x] + ?[y]` works.
 - `Unset Intuition Negation Unfolding` will cause `intuition` to stop unfolding `not`.
@@ -167,7 +167,7 @@ To build all the examples in `src/`, run `make`.
 - A useful convention for notations is to have them start with a word and an exclamation mark. This is borrowed from @andres-erbsen, who borrowed it from the Rust macro syntax. An example of using this convention is in [Macros.v](src/Macros.v). There are three big advantages to this approach: first, using it consistently alerts readers that a macro is being used, and second, using names makes it much easier to create many macros compared to inventing ASCII syntax, and third, starting every macro with a keyword makes them much easier to get parsing correctly.
 - To declare an axiomatic instance of a typeclass, use `Declare Instance foo : TypeClass`. This better than the pattern of `Axiom` + `Existing Instance`.
 - To make Ltac scripts more readable, you can use `Set Default Goal Selector "!".`, which will enforce that every Ltac command (sentence) be applied to exactly one focused goal. You achieve that by using a combination of bullets and braces. As a result, when reading a script you can always see the flow of where multiple goals are generated and solved.
-- `Arguments foo _ & _` (in Coq 8.11) adds a _bidirectionality hint_ saying that an application of `foo` should infer a type from its arguments after typing the first argument. See [Bidirectional.v](src/Bidirectional.v) for an example and the [latest Coq documentation](https://coq.github.io/doc/master/refman/language/gallina-extensions.html?highlight=bidirectional#coq:cmd.arguments-bidirectionality-hints).
+- `Arguments foo _ & _` (in Coq 8.11) adds a _bidirectionality hint_ saying that an application of `foo` should infer a type from its arguments after typing the first argument. See [Bidirectional.v](src/Bidirectional.v) for an example and the [latest Coq documentation](https://rocq-prover.org/doc/master/refman/language/extensions/arguments-command.html#bidirectionality-hints).
 - Coq 8.11 introduced compiled interfaces, aka `vos` files (as far as I can tell they are a more principled replacement for `vio` files). Suppose you make a change deep down to `Lib.v` and want to start working on `Proof.v` which imports `Lib.v` through many dependencies. With `vos` files, you can recompile all the _signatures_ that `Proof.v` depends on, skippinng proofs, and keep working. The basic way to use them is to compile `Proof.required_vos`, a special dependency `coqdep` generates that will build everything needed to work on `Proof.v`. Coq natively looks for `vos` files in interactive mode, and uses empty `vos` files to indicate that the file is fully compiled in a `vo` file.
 
   Note that Coq also has `vok` files; it's possible to check the missing proofs in a `vos` file, but this does not produce a `vo` and so all Coq can do is record that the proofs have been checked. They can also be compiled in parallel within a single file, although I don't know how to do that. Compiling `vok`s lets you fairly confidently check proofs, but to really check everything (particularly universe constraints) you need to build `vo` files from scratch.
@@ -206,7 +206,7 @@ To build all the examples in `src/`, run `make`.
 - You can pass `-noinit` to `coqc` or `coqtop` to avoid loading the standard library.
 - Ltac is provided as a plugin loaded by the standard library; if you have `-noinit` to load it you need `Declare ML Module "ltac_plugin".` (see [NoInit.v](src/NoInit.v)).
 - Numeral notations are only provided by the prelude, even if you issue `Require Import Coq.Init.Datatypes`.
-- If you use Coq master, the latest Coq reference manual is built and deployed to <https://coq.github.io/doc/master/refman/index.html> automatically.
+- If you use Coq master, the latest Coq reference manual is built and deployed to <https://rocq-prover.org/doc/master/refman/index.html> automatically.
 - At Qed, Coq re-checks the proof term, which can take a while. At the same
   time, Qed rarely fails - some reasons why it might include that there's a
   universe inconsistency, the coinductive guarded check fails, there's a bug in

mlc_config.json

@@ -0,0 +1,10 @@
+{
+  "ignorePatterns": [
+    {
+      "pattern": "^https://stackoverflow.com/questions/.*"
+    },
+    {
+      "pattern": "^https://img.shields.io/badge/.*"
+    }
+  ]
+}