Merge branch 'master' into jaroslav/UnsatCores

.github/CODEOWNERS

@@ -0,0 +1 @@
+/docs/gambit/gambit.md @chandrakananandi

.github/workflows/check.yml

@@ -6,7 +6,9 @@ jobs:
   docs:
     runs-on: ubuntu-latest
     steps:
-    - uses: actions/checkout@v1
+    - uses: actions/checkout@v4
+      with:
+        submodules: 'recursive'
     - uses: actions/setup-python@v4
       with:
         python-version: '3.10'
@@ -15,5 +17,5 @@ jobs:
     - run: pip3 install -r requirements.txt
     - run: make spelling
     - run: |
-        find build/spelling -type f | xargs cat > errors.txt
+        find build/spelling -path *.spelling -type f | xargs cat > errors.txt
         [[ ! $(cat errors.txt) ]] || (echo && echo "errors:" && cat errors.txt && false)

.gitignore

@@ -1,4 +1,15 @@
+# Repo specifics
 build
+
+# Python
 __pycache__
-.certora_internal
 **/__pycache__
+
+# Certora
+.certora_internal/
+.certora_recent_jobs.json
+.zip-output-url.txt
+
+# vim
+.*.swp
+.*.swo

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "docs/user-guide/multicontract/LiquidityPoolExample"]
-	path = docs/user-guide/multicontract/LiquidityPoolExample
-	url = https://github.com/Certora/LiquidityPoolExample.git
 [submodule "docs/cvl/cvl2/cvl1"]
 	path = docs/cvl/cvl2/cvl1
 	url = [email protected]:Certora/CVL2Migration.git
@@ -9,3 +6,6 @@
 	path = docs/cvl/cvl2/cvl2
 	url = [email protected]:Certora/CVL2Migration.git
 	branch = cvl2
+[submodule "Examples"]
+	path = Examples
+	url = https://github.com/Certora/Examples.git

.readthedocs.yaml

@@ -3,7 +3,7 @@ version: 2
 build:
   os: "ubuntu-22.04"
   tools:
-    python: "3.8"
+    python: "3.10"
 
 python:
   install:
@@ -14,3 +14,14 @@ sphinx:
   configuration: conf.py
   fail_on_warning: true
 
+# Submodules
+submodules:
+  include:
+    - Examples
+  recursive: true
+
+search:
+  ranking:
+    docs/confluence/*: -7
+    docs/whitepaper/*: -6
+    docs/equiv-check/*: -8

_requirements.txt

@@ -0,0 +1,8 @@
+# The basic requirements file used by pip-compile 
+sphinx~=7.4.5
+myst-parser
+sphinx-rtd-theme
+sphinxcontrib-spelling
+sphinx-copybutton
+
+git+https://github.com/Certora/docs-infrastructure.git@master#egg=docsinfra

conf.py

@@ -12,74 +12,101 @@
 
 import os
 import sys
-sys.path.insert(0, os.path.abspath('./util'))
+
+from docsinfra.sphinx_utils import TAGS, CVL2Lexer
+
+sys.path.insert(0, os.path.abspath("./util"))
+
 
 # -- Project information -----------------------------------------------------
 
-project = 'Certora Prover Documentation'
-copyright = '2022, Certora, Inc'
-author = 'Certora, Inc'
+project = "Certora Prover Documentation"
+copyright = "2024, Certora, Inc"
+author = "Certora, Inc"
 
 # The full version, including alpha/beta/rc tags
-release = '0.0'
+release = "0.0"
 
 
 # -- General configuration ---------------------------------------------------
 
-import sphinx_rtd_theme
-
 # Add any Sphinx extension module names here, as strings. They can be
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
-    'myst_parser',
-    'sphinx_rtd_theme',
-    'sphinx.ext.todo',
+    "myst_parser",
+    "sphinx.ext.todo",
+    "sphinx_rtd_theme",
+    "sphinx_design",
+    "docsinfra.sphinx_utils.codelink_extension",
+    "docsinfra.sphinx_utils.includecvl",
+    "sphinx_copybutton"
 ]
 
 # Add any paths that contain templates here, relative to this directory.
-templates_path = ['templates']
+templates_path = ["templates"]
 
 # List of patterns, relative to source directory, that match files and
 # directories to ignore when looking for source files.
 # This pattern also affects html_static_path and html_extra_path.
 exclude_patterns = [
-    '_build',
-    'templates',
-    'Thumbs.db',
-    '.DS_Store',
-    'old',
-    'README.md',
-    'EVMVerifier',
-    'docs/cvl/Test/*',
-    'docs/user-guide/multicontract/LiquidityPoolExample',
-    'docs/cvl/cvl2/CVL2Examples',
-    'docs/cvl/cvl2/cvl1',
-    'docs/cvl/cvl2/cvl2',
-    '.github'
-    ]
+    "_build",
+    "templates",
+    "Thumbs.db",
+    ".DS_Store",
+    "old",
+    "README.md",
+    "EVMVerifier",
+    "docs/cvl/Test/*",
+    "docs/user-guide/multicontract/LiquidityPoolExample",
+    "docs/cvl/cvl2/CVL2Examples",
+    "docs/cvl/cvl2/cvl1",
+    "docs/cvl/cvl2/cvl2",
+    ".github",
+    "Examples/*",
+]
 
 
 # -- Options for HTML output -------------------------------------------------
 
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = 'sphinx_rtd_theme'
+html_theme = "sphinx_rtd_theme"
 
 # Add any paths that contain custom static files (such as style sheets) here,
 # relative to this directory. They are copied after the builtin static files,
 # so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ['static']
+html_static_path = ["static"]
+
+# The Certora logo
+html_logo = "static/Certora_Logo_Black.svg"
+
+
+# -- codelink_extension configuration ----------------------------------------
+code_path_override = "Examples/"
+link_to_github = True
+
+
+# -- prologue and epilog -------------------------------------------------------
+# A string of reStructuredText that will be included at the beginning of every source
+# file that is read.
+# Here we use the prologue to add inline cvl code and solidity code.
+rst_prolog = """
+.. role:: cvl(code)
+   :language: cvl
+
+.. role:: solidity(code)
+   :language: solidity
+"""
+
 
 # -- Custom setup ------------------------------------------------------------
 
-todo_include_todos = True
+# Do not show todo list unless in dev build
+todo_include_todos = tags.has(TAGS.is_dev_build)  # noqa: F821
 
-def setup(sphinx):
-    sphinx.add_css_file('custom.css')
-    from highlight import CVLLexer
-    sphinx.add_lexer("cvl", CVLLexer)
-    from pygments_lexer_solidity import SolidityLexer
-    sphinx.add_lexer("solidity", SolidityLexer)
 
+def setup(sphinx):
+    sphinx.add_css_file("custom.css")
+    sphinx.add_lexer("cvl", CVL2Lexer)