Fix broken code links in docs

docs/editor.md

@@ -5,7 +5,7 @@ If you really want to, you can also avoid having to type unicode characters by
 importing `iris.bi.ascii`.  That enables parsing-only ASCII alternatives to many
 unicode notations. (Feel free to report an issue when you notice that a notation
 is missing.)  The easiest way to learn the ASCII syntax is to
-[read this file](/iris/bi/ascii.v).
+[read this file](../iris/bi/ascii.v).
 Note however that this will make your code harder to read and work on for Iris
 developers that are used to our default unicode notation---generally, our
 recommendation is to use the unicode syntax whenever possible. In particular,

docs/heap_lang.md

@@ -128,7 +128,7 @@ all of the redexes reduced.)
 Sometimes, it is useful to define a derived notion in HeapLang that involves
 thunks.  For example, the parallel composition `e1 ||| e2` is definable in
 HeapLang, but that requires thunking `e1` and `e2` before passing them to
-`par`. (This is defined in [`par.v`](theories/heap_lang/lib/par.v).)  However,
+`par`. (This is defined in [`par.v`](../iris_heap_lang/lib/par.v).)  However,
 this is somewhat subtle because of the distinction between expression lambdas
 and value lambdas.
 

docs/proof_mode.md

@@ -21,7 +21,7 @@ pervasively. These are defined in dedicated sections in this manual.
 
 Many of the tactics below apply to more goals than described in this document
 since the behavior of these tactics can be tuned via instances of the type
-classes in the file [proofmode/classes](iris/proofmode/classes.v). Most notably, many
+classes in the file [proofmode/classes](../iris/proofmode/classes.v). Most notably, many
 of the tactics can be applied when the connective to be introduced or to be eliminated
 appears under a later, an update modality, or in the conclusion of a
 weakest precondition.

docs/resource_algebras.md

@@ -99,7 +99,7 @@ To obtain a closed Iris proof, i.e., a proof that does not make assumptions like
 `inG`, you have to assemble a list of functors of all the involved modules,
 and if your proof relies on some singleton (most do, at least indirectly; also
 see the next section), you have to call the respective initialization or
-adequacy lemma.  [For example](tests/one_shot.v):
+adequacy lemma.  [For example](../tests/one_shot.v):
 ```coq
 Section client.
   Context `{!heapGS Σ, !one_shotG Σ, !spawnG Σ}.
@@ -142,9 +142,9 @@ would be incompatible with each other.
 
 The `gen_heapGpreS` typeclass (without the singleton data) is relevant for
 initialization, i.e., to create an instance of `gen_heapGS`. This is happening as
-part of [`heap_adequacy`](iris_heap_lang/adequacy.v) using the
+part of [`heap_adequacy`](../iris_heap_lang/adequacy.v) using the
 initialization lemma for `gen_heapGS` from
-[`gen_heap_init`](iris/base_logic/lib/gen_heap.v):
+[`gen_heap_init`](../iris/base_logic/lib/gen_heap.v):
 ```coq
 Lemma gen_heap_init `{gen_heapGpreS L V Σ} σ :
   (|==> ∃ _ : gen_heapGS L V Σ, gen_heap_ctx σ)%I.
@@ -232,9 +232,9 @@ F (X,X⁻) := gmap K (agree (nat * ▶ X))
 To make it convenient to construct such functors and prove their contractivity,
 we provide a number of abstractions:
 
-- [`oFunctor`](iris/algebra/ofe.v): functors from COFEs to OFEs.
-- [`rFunctor`](iris/algebra/cmra.v): functors from COFEs to cameras.
-- [`urFunctor`](iris/algebra/cmra.v): functors from COFEs to unital
+- [`oFunctor`](../iris/algebra/ofe.v): functors from COFEs to OFEs.
+- [`rFunctor`](../iris/algebra/cmra.v): functors from COFEs to cameras.
+- [`urFunctor`](../iris/algebra/cmra.v): functors from COFEs to unital
   cameras.
 
 Besides, there are the classes `oFunctorContractive`, `rFunctorContractive`, and