Fix typos, links in docs (#94)

docs/eval_modes/options.md

@@ -8,11 +8,11 @@ nav_order: 1
 # Options and System Properties 
 
 Formulog evaluation is controlled by options and system properties.
-For example, to interpret the test program with SMT debug information (the `debugSmt` property) and 2
-threads (the `-j 2` option), use
+For example, to interpret the test program with SMT logging and 2
+threads, use the `debugSmt` property and `-j 2` option:
 
 ```
-java -DdebugSmt -jar formulog.jar greeting.flg -j 2
+java -DdebugSmt -jar formulog.jar example/greeting.flg -j 2
 ```
 
 ## Options

docs/eval_modes/smt.md

@@ -23,7 +23,7 @@ SMT solving).
 - `push-pop`: try to use incremental SMT solving via the `push` and `pop` SMT
 commands. This can work well when query `y` extends query `x`; e.g., `y = c ::
 x`, where `c` is an additional conjunct; this situation most commonly occurs
-when using [eager evaluation]({{ site.baseurl }}{% link eval_modes/eager.md %}).
+when using [eager evaluation]({{ site.base_url }}{% link eval_modes/eager.md %}).
 - `check-sat-assuming`: try to use incremental SMT solving via the
 `check-sat-assuming` SMT command. This caches conjuncts in the SMT solver in a
 way such that they can be enabled or disabled per SMT query, and works well if

docs/lang_ref/goal_directed_eval.md

@@ -49,7 +49,7 @@ predicates that are "invoked" from the functional fragment of Formulog.
 
 Queries are in the form `:- A.` where `A` is a positive (non-negated) atom. The
 typical rules about variable usage apply (see the "Anonymous variables" section
-of the [Program Safety page]({{ site.baseurl }}{% link lang_ref/program_safety.md %})). If you want to have a query consisting of
+of the [Program Safety page]({{ site.base_url }}{% link lang_ref/program_safety.md %})). If you want to have a query consisting of
 multiple atoms, write a rule defining a new relation and then query that
 relation. For example, the hypothetical query `:- A, B.` could be rewritten as
 the rule `R :- A, B.` and query `:- R.`. There can be only one query per

docs/lang_ref/lang_basics.md

@@ -53,7 +53,7 @@ type cmp =
 ```
 
 It also has built-in types representing logical formulas, but a discussion of
-these is delayed until the [section on logical formulas]({{ site.baseurl }}{% link lang_ref/logical_formulas.md %}).
+these is delayed until the [section on logical formulas]({{ site.base_url }}{% link lang_ref/logical_formulas.md %}).
 
 #### List Notation
 
@@ -421,7 +421,7 @@ with manipulating primitives):
   respectively. The string should either be a decimal integer preceded
   optionally by `-` or `+`, or a hexadecimal integer preceded by `0x`. The
   operations return `none` if the string is not in the proper format or
-  represents an integer too large to fit in 32/64 bits.
+  represents an integer of too great magnitude to fit in 32/64 bits.
 
 Standard arithmetic notation can be used for signed `i32` operations. For
 example, `38 + 12 / 3` is shorthand for `i32_add(38, i32_sdiv(12, 3))`.

docs/lang_ref/logical_formulas.md

@@ -467,4 +467,4 @@ finds one in time; it returns `none` otherwise. Variables in a model can be
 inspected using `query_model`, which will return
 `none` if a variable is not present in the model or if it is of a type that
 cannot be concretely represented in Formulog (for example, Formulog does not
-have a concrete representation of a 13-bit bit vector).
+have a concrete representation of a 13-bit vector).

docs/starting.md

@@ -9,7 +9,7 @@ nav_order: 2
 Thank you for your interest in Formulog!
 This page describes how to set up Formulog and provides some pointers on writing Formulog programs.
 
-## Seting up Formulog
+## Setting up Formulog
 
 There are three main ways to set up Formulog (listed in increasing order of number of dependencies):
 
@@ -100,15 +100,15 @@ greeting("Hello, World")
 
 Now that you have Formulog set up, the fun part starts: writing Formulog programs!
 
-Check out our [tutorial]({{ site.baseurl }}{% link tutorial/index.md %}) for a walk-through of how to encode a refinement type system in Formulog.
+Check out our [tutorial]({{ site.base_url }}{% link tutorial/index.md %}) for a walk-through of how to encode a refinement type system in Formulog.
 Additional short-ish example programs can be found in the `examples/` directory (in the Docker image or repository base directory).
 For examples of larger developments, see the case studies we have used in publications:
 
 - [a refinement type checker](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/dminor/bench.flg)
 - [a bottom-up points-to analysis for Java](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/scuba/bench.flg)
 - [a symbolic executor an LLVM fragment](https://github.com/aaronbembenek/making-formulog-fast/blob/main/benchmarks/symex/bench.flg)
 
-See the [language reference]({{ site.baseurl }}{% link lang_ref/index.md %}) for details about Formulog constructs.
+See the [language reference]({{ site.base_url }}{% link lang_ref/index.md %}) for details about Formulog constructs.
 
 Syntax highlighting is available for Visual Studio Code (follow instructions [here](https://github.com/HarvardPL/formulog-syntax)) and Vim (install [misc/flg.vim](https://github.com/HarvardPL/formulog/blob/master/misc/flg.vim)).
 

docs/tutorial/index.md

@@ -7,7 +7,7 @@ nav_order: 3
 # Tutorial: Building a Refinement Type Checker
 
 In this tutorial, we'll implement a type checker for a small (but still interesting) refinement type system in Formulog.
-In particular, we'll implement the declarative, bidirectional type checking rules for the first system in the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763) by Ranjit Jhala and Niki Vazou [1].
+In particular, we'll implement the declarative, bidirectional type checking rules for the first system in the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763v1) by Ranjit Jhala and Niki Vazou [1].
 Our hope is that our tutorial gives a good overview of many Formulog features, and a flavor of what it is like to program a nontrivial analysis in Formulog.
 
 ### Intended Audience
@@ -24,7 +24,7 @@ If you have a question about the content of this tutorial, a suggestion for impr
 
 ### Attribution
 
-This tutorial includes figures from the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763) (v1) by Ranjit Jhala and Niki Vazou [1], which has been published under a [CC BY 4.0 license](https://creativecommons.org/licenses/by/4.0/).
+This tutorial includes figures from the article [Refinement Types: A Tutorial](https://arxiv.org/abs/2010.07763v1) by Ranjit Jhala and Niki Vazou [1], which has been published under a [CC BY 4.0 license](https://creativecommons.org/licenses/by/4.0/).
 We will refer to this article as "JV" for short.
 
 ## General Approach
@@ -35,7 +35,7 @@ Our typical approach when implementing an analysis in Formulog is thus to try to
 
 This is the approach we will follow in this tutorial: directly translate the formalism of JV as we encounter it, and then go back to patch our implementation as necessary.
 Concretely, we will work our way through JV Sections 3.1 and 3.2.
-For the full, final code, see [tutorial.flg](tutorial.flg).
+For the full, final code, see [tutorial.flg](https://github.com/HarvardPL/formulog/blob/master/docs/tutorial/tutorial.flg).
 
 ## Definitions
 
@@ -600,7 +600,7 @@ ent((X, t_refined(B, Y, P)) :: G, C) :-
 ```
 
 Now the type checker works on this example!
-(This isn't the most general solution: a better technique would be to create a fresh variable and substitute it with `Y` in `P` and `X` in `C`; however, this is good enough for now.)
+(This isn't the most general solution: a better technique would be to create a fresh variable and substitute it for `Y` in `P` and `X` in `C`; however, this is good enough for now.)
 
 ### Checking Functions
 
@@ -772,10 +772,10 @@ As we mentioned earlier, please raise a [GitHub issue](https://github.com/Harvar
 
 ## References
 
-[1] Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. arXiv:2010.07763. https://arxiv.org/abs/2010.07763
+[1] Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. arXiv:2010.07763v1. <https://arxiv.org/abs/2010.07763v1>
 
-[2] Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. 2012. Semantic Subtyping with an SMT Solver. Journal of Functional Programming 22, 1 (2012), 31–105. https://doi.org/10.1145/1863543.1863560
+[2] Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. 2012. Semantic Subtyping with an SMT Solver. Journal of Functional Programming 22, 1 (2012), 31–105. <https://doi.org/10.1017/S0956796812000032>
 
-[3] Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-up Context-Sensitive Pointer Analysis for Java. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems. 465–484. https://doi.org/10.1007/978-3-319-26529-2_25
+[3] Yu Feng, Xinyu Wang, Isil Dillig, and Thomas Dillig. 2015. Bottom-up Context-Sensitive Pointer Analysis for Java. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems. 465–484. <https://doi.org/10.1007/978-3-319-26529-2_25>
 
-[4] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209–224. https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf
+[4] Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. 209–224. <https://www.usenix.org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf>

docs/tutorial/tutorial.flg

@@ -2,7 +2,7 @@
 DEFINITIONS
 *******************************************************************************)
 
-(* An algebraic data type with a single variant *)
+(* An algebraic data type with two variants *)
 type basic_typ =
     | b_int
     | b_bool
@@ -39,7 +39,7 @@ type kind =
     | k_base
     | k_star
 
-(* Tuples and lists are built-in type *)
+(* Tuples and lists are built-in types *)
 type env = (var * typ) list
 
 type expr =