cn-tutorial/mkdocs.yml at main · rems-project/cn-tutorial · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
site_name: CN Docs
site_dir: build
repo_url: https://github.com/rems-project/cn-tutorial
repo_name: rems-project/cn-tutorial
edit_uri: edit/main/docs
theme:
  name: material
  features:
    - announce.dismiss
    - content.action.edit
    - content.action.view
    - content.code.annotate
    - content.code.copy
    # - content.code.select
    - content.tooltips
    - navigation.footer
    # - navigation.indexes
    # - navigation.instant
    # - navigation.instant.prefetch
    # - navigation.instant.progress
    # - navigation.prune
    # - navigation.sections
    - navigation.tabs
    - navigation.top
    - navigation.tracking
    - search.highlight
    - search.share
    - search.suggest
    - toc.follow
    - toc.integrate
  language: en
  palette:
    - media: "(prefers-color-scheme)"
      toggle:
        icon: material/link
        name: Switch to light mode
    - media: "(prefers-color-scheme: light)"
      scheme: default
      primary: indigo
      accent: indigo
      toggle:
        icon: material/toggle-switch
        name: Switch to dark mode
    - media: "(prefers-color-scheme: dark)"
      scheme: slate
      primary: black
      accent: indigo
      toggle:
        icon: material/toggle-switch-off
        name: Switch to system preference
  font:
    text: Roboto
    code: Roboto Mono
  icon:
    repo: fontawesome/brands/github

plugins:
  - search
  - macros:
      module_name: macros

hooks:
  - hooks.py

# Extensions
markdown_extensions:
  - abbr
  - admonition
  - attr_list
  - def_list
  - md_in_html
  - toc:
      permalink: true
  - pymdownx.arithmatex:
      generic: true
  - pymdownx.betterem:
      smart_enable: all
  - pymdownx.caret
  - pymdownx.details
  - pymdownx.emoji:
      emoji_generator: !!python/name:material.extensions.emoji.to_svg
      emoji_index: !!python/name:material.extensions.emoji.twemoji
  - pymdownx.highlight:
      anchor_linenums: true
      line_spans: __span
      pygments_lang_class: true
  - pymdownx.inlinehilite
  - pymdownx.keys
  - pymdownx.mark
  - pymdownx.smartsymbols
  - pymdownx.snippets:
      base_path: ["docs", "build"]
  - pymdownx.striphtml
  - pymdownx.superfences:
      custom_fences:
        - name: mermaid
          class: mermaid
          format: !!python/name:pymdownx.superfences.fence_code_format
  - pymdownx.tabbed:
      alternate_style: true
      combine_header_slug: true
      slugify: !!python/object/apply:pymdownx.slugs.slugify
        kwds:
          case: lower
  - pymdownx.tasklist:
      custom_checkbox: true
  - pymdownx.tilde

# # Page tree
nav:
  - Home: README.md

  - Docs:
    - Getting Started:
      - getting-started/installation.md

    - A Tour of CN:
      - getting-started/tutorials/welcome.md
      - getting-started/tutorials/first-taste.md
      - getting-started/tutorials/verif-basics.md
      - getting-started/tutorials/pointers.md
      - getting-started/tutorials/verif-pointers.md
      - getting-started/tutorials/arrays.md
      - getting-started/tutorials/verif-arrays.md
      - getting-started/tutorials/alloc.md
      - getting-started/tutorials/verif-alloc.md
      - getting-started/tutorials/predicates.md
      - getting-started/tutorials/verif-lists.md
      - getting-started/tutorials/verif-splitcase.md

    - More on Testing:
      - getting-started/tutorials/unit-testing.md
      - getting-started/tutorials/test-distribs.md

    - More on Verification:
      - getting-started/tutorials/verif-numeric.md
      - getting-started/tutorials/verif-external.md

    - Case Studies:
      - getting-started/case-studies/imperative-queues.md
      - getting-started/case-studies/verif-imperative-queues.md
      - getting-started/case-studies/doubly-linked-lists.md
      - getting-started/case-studies/verif-doubly-linked-lists.md
      - getting-started/case-studies/the-runway.md
      - getting-started/case-studies/verif-the-runway.md

  - Reference:
    - reference/README.md
    - specifications/README.md
    - specifications/function-specifications.md
    - specifications/loop-invariants.md
    - specifications/conditions.md
    - specifications/expressions.md
    - specifications/resource-predicates.md
    - Auxiliary definitions:
      - specifications/auxiliary-definitions/README.md
      - specifications/auxiliary-definitions/data-structures.md
      - specifications/auxiliary-definitions/logical-functions.md
      - specifications/auxiliary-definitions/custom-resource-predicates.md
    - specifications/types.md
    - specifications/scoping.md
    - specifications/tactics.md
    - specifications/interactive-theorem-proving.md