Fix outdated URLs

CHANGES.md

@@ -821,13 +821,13 @@
 
  * speed up by using constants instead of uninterpreted functions
 
- * options for fine tuning with `--fine-tuning`, see [tuning](https://github.com/informalsystems/apalache/blob/unstable/docs/tuning.md)
+ * options for fine tuning with `--fine-tuning`, see [tuning](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/tuning.md)
 
  * bugfix in logback configuration
 
 ## 0.4.0-pre1
 
- * type annotations and very simple type inference, see the [notes](https://github.com/informalsystems/apalache/blob/unstable/docs/types-and-annotations.md)
+ * type annotations and very simple type inference, see the [notes](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/types-and-annotations.md)
 
  * a dramatic speed up of many operators by using a `QF_NIA` theory and cherry pick
 

build.sbt

@@ -21,7 +21,7 @@ ThisBuild / version := scala.io.Source.fromFile(versionFile.value).mkString.trim
 ThisBuild / organization := "at.forsyte"
 ThisBuild / scalaVersion := "2.13.8"
 
-// https://oss.sonatype.org/content/repositories/snapshots/
+// Add resolver for Sonatype OSS Snapshots Maven repository
 ThisBuild / resolvers += Resolver.sonatypeRepo("snapshots")
 
 // Shared dependencies accross all sub projects

docs/src/adr/004adr-annotations.md

@@ -144,7 +144,7 @@ FactFun[n \in Int] ==
 
 The implementation of the annotation parser can be found in the class
 `at.forsyte.apalache.io.annotations.AnnotationParser` of the module
-`tla-import`, see [AnnotationParser][].
+`tla-io`, see [AnnotationParser][].
 
 ## 5. Discussion
 
@@ -163,5 +163,5 @@ so it would be otherwise impossible to find the end of an annotation.
 
 [Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8
 
-[AnnotationParser]: https://github.com/informalsystems/apalache/blob/unstable/tla-import/src/main/scala/at/forsyte/apalache/io/annotations/AnnotationParser.scala
+[AnnotationParser]: https://github.com/informalsystems/apalache/blob/unstable/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/AnnotationParser.scala
 

docs/src/adr/010rfc-transition-explorer.md

@@ -52,7 +52,7 @@ In the current architecture, there is a single mode of operation in which
   specification,
 - the specification and configurations are parsed and pre-processed,
 - and then the model checker proper drives the
-  [TransitionExecutor](../../src/adr/003adr-trex.md) to effect symbolic
+  [TransitionExecutor](./003adr-trex.md) to effect symbolic
   executions verifying the specified properties for the specified model.
 
 This RFC proposes the addition of a *symbolic transition exploration server*.

docs/src/apalache/features.md

@@ -4,7 +4,7 @@ Here is the list of the TLA+ language features that are currently supported by A
 
 At the moment, Apalache is able to check state invariants, action invariants,
 trace invariants as well as inductive invariants. (See the [page on
-invariants](https://apalache.informal.systems/docs/apalache/invariants.html) in
+invariants](https://apalache.informal.systems/docs/apalache/principles/invariants.html) in
 the manual.) Which means that you can only check safety properties with
 Apalache, unless you employ a [liveness-to-safety] transformation in your spec.
 In general, we do not support checking liveness properties.  If you would like

docs/src/apalache/installation/docker.md

@@ -80,7 +80,7 @@ The development of Apalache proceeds at a high pace, and we introduce a
 substantial number of improvements in the unstable branch before the next stable
 release. Please refer to the [change
 log](https://github.com/informalsystems/apalache/blob/unstable/CHANGES.md) and
-[manual](https://github.com/informalsystems/apalache/blob/unstable/docs/src/manual.md)
+[manual](https://github.com/informalsystems/apalache/blob/unstable/docs/src/apalache/index.md)
 on the unstable branch for the description of the newest features. **We
 recommend using the unstable version if you want to try all the exciting new
 features of Apalache. But be warned: It is called "unstable" for a reason**. To

docs/src/apalache/principles/assignments.md

@@ -70,8 +70,8 @@ Apalache reports an error as follows:
 ```console
 ...
 PASS #9: TransitionFinderPass
-To understand the error, check the manual:
-[https://apalache.informal.systems/docs/apalache/assignments.html]
+To understand the error, [check the
+manual](https://apalache.informal.systems/docs/apalache/principles/assignments.html):
 Assignment error: No assignments found for: a
 It took me 0 days  0 hours  0 min  1 sec
 Total time: 1.88 sec

docs/src/lang/sequences.md

@@ -577,7 +577,7 @@ till the end of the universe.
 [Control Flow and Non-determinism]: ./control-and-nondeterminism.md
 [Specifying Systems]: http://lamport.azurewebsites.net/tla/book.html?back-link=learning.html
 [Paxos]: https://github.com/tlaplus/Examples/blob/master/specifications/Paxos/Paxos.tla
-[Apalache ADR002]: https://github.com/informalsystems/apalache/blob/unstable/docs/adr/002adr-types.md
+[Apalache ADR002]: https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/002adr-types.md
 [Cartesian product]: https://en.wikipedia.org/wiki/Cartesian_product
 [Overriding Seq in TLC]: https://groups.google.com/g/tlaplus/c/sYx_6e3YyWk/m/4CnwPqIVAgAJ
 [HOWTO write type annotations]: ../../HOWTOs/howto-write-type-annotations.md

src/tla/Apalache.tla

@@ -24,7 +24,7 @@
  * assignments by hand, you can use this operator.
  *
  * For a further discussion on that matter, see:
- * https://github.com/informalsystems/apalache/blob/ik/idiomatic-tla/docs/idiomatic/assignments.md
+ * https://github.com/informalsystems/apalache/blob/unstable/docs/src/idiomatic/001assignments.md
  *)
 x := e == x = e
 

test/tla/SafeMath.tla

@@ -5,7 +5,7 @@
  *
  * Here we are testing SafeMath:
  *
- * https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/math/SafeMath.sol
+ * https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/math/SafeMath.sol
  *
  * More on the topic:
  *

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala

@@ -195,7 +195,7 @@ class SmtFreeSymbolicTransitionExtractor(
 }
 
 object SmtFreeSymbolicTransitionExtractor {
-  val MANUAL_LINK = "https://apalache.informal.systems/docs/apalache/principles.html#assignments"
+  val MANUAL_LINK = "https://apalache.informal.systems/docs/apalache/principles/assignments.html"
 
   def apply(tracker: TransformationTracker, sourceLoc: SourceLocator): SmtFreeSymbolicTransitionExtractor = {
     new SmtFreeSymbolicTransitionExtractor(tracker, sourceLoc)

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala

@@ -48,7 +48,7 @@ class CheckerExceptionAdapter @Inject() (sourceStore: SourceStore, changeListene
 
     case err: AssignmentException =>
       logger.info("To understand the error, read the manual:")
-      logger.info("  [https://apalache.informal.systems/docs/apalache/assignments.html]")
+      logger.info("  [https://apalache.informal.systems/docs/apalache/principles/assignments.html]")
       NormalErrorMessage("Assignment error: " + err.getMessage)
 
     case err: OutdatedAnnotationsError =>

tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaType1.scala

@@ -4,7 +4,7 @@ import scala.collection.immutable.SortedMap
 
 /**
  * Trait for a type in Type System 1 as specified in <a
- * href="https://github.com/informalsystems/apalache/blob/unstable/docs/adr/002adr-types.md">ADR-002</a>.
+ * href="https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/002adr-types.md">ADR-002</a>.
  *
  * It also contains experimental extensions that are specified in <a
  * href="https://github.com/informalsystems/apalache/blob/unstable/docs/src/adr/014adr-precise-records.md">ADR-014</a>.