mkdocs.yml

site_name: Lean Prover 中文文档
site_url: https://leanprover.cn
repo_url: https://github.com/Lean-zh/Lean-zh.github.io
repo_name: Lean-zh
edit_uri: edit/main/docs/

theme:
  name: material
  palette:
    primary: green
    accent: light green
  font:
    text: Roboto
    code: Roboto Mono
  features:
    - navigation.tabs
    - navigation.sections
    - navigation.instant
    - search.highlight
    - search.share
    - content.code.copy
    - content.code.annotate

plugins:
  - search:
      lang: zh
  - minify:
      minify_html: true

markdown_extensions:
  - admonition
  - codehilite:
      guess_lang: false
  - toc:
      permalink: true
  - pymdownx.arithmatex:
      generic: true
  - pymdownx.betterem:
      smart_enable: all
  - pymdownx.highlight:
      use_pygments: true
      pygments_style: friendly
  - pymdownx.caret
  - pymdownx.critic
  - pymdownx.details
  - pymdownx.emoji
  - pymdownx.inlinehilite
  - pymdownx.magiclink
  - pymdownx.mark
  - pymdownx.smartsymbols
  - pymdownx.superfences
  - pymdownx.tasklist:
      custom_checkbox: true
  - pymdownx.tilde

extra_javascript:
  - https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS-MML_HTMLorMML

extra_css:
  - assets/css/custom.css
  - https://cdnjs.cloudflare.com/ajax/libs/font-awesome/5.15.4/css/all.min.css

extra:
  version:
    provider: mike
    default: latest
    alias: true

nav:
  - 主页: 
    - Lean-zh: index.md
    - 安装指南: install.md
    - Lean4 工具链: tutorial/elan-lake.md
    - Lake 包管理: references/lake-doc.md
    - 项目示例 - 元编程: projects/meta-example.md
  - 交互工具:
    - 交互工具: tool/index.md
    - LeanDojo 教程: tool/lean-dojo.md
    - REPL 教程: tool/repl.md
    - Polyrith 策略: tool/polyrith.md
    - PantoGraph 教程: tool/pantograph.md
  - 项目教程:
    - Lean4web 在线编译器: projects/lean4web.md
    - jixia 数据分析: projects/jixia.md
    - Lean4Game 教程: projects/lean4game.md
  - 贡献指南: contributing.md