manifest.yaml

nav:
  rootSlug: introduction
  sections:
  - name: 'A quick tour'
    notebookSlug: welcome
  - name: 'Installation'
    notebookSlug: installation
    children:
    - name: 'Installer'
      notebookSlug: installation-simple
    - name: 'Manual (opam)'
      notebookSlug: installation-manual-opam
    - name: 'Docker Image'
      notebookSlug: installation-docker
    - name: 'Jupyter Notebook'
      notebookSlug: installation-jupyter
    - name: 'VSCode'
      notebookSlug: installation-vscode
    - name: 'Server Image'
      notebookSlug: installation-server-image
  - name: 'Logic and Program modes'
    notebookSlug: logic-and-program-modes
  - name: 'Verification'
    notebookSlug: verification
    children:
      - name: "Commands"
        notebookSlug: verification-commands
      - name: "Attributes"
        notebookSlug: verification-attributes
      - name: 'Unrolling'
        notebookSlug: verification-unrolling
      - name: 'Simplification'
        notebookSlug: verification-simplification
      - name: 'Blast'
        notebookSlug: verification-blast
      - name: 'Induction'
        notebookSlug: verification-induction
      - name: 'Waterfall'
        notebookSlug: verification-waterfall
  - name: 'Proving program termination'
    notebookSlug: proving-program-termination
  - name: 'Region Decomposition'
    notebookSlug: decomposition
    children:
    - notebookSlug: decomposition-intro
      name: "Background to decomposition"
    - notebookSlug: imandra-tools-intro
      name: 'Imandra tools introduction'
    - notebookSlug: idf
      name: 'Iterative Decomposition Framework'
    - notebookSlug: region-probabilities
      name: 'Region Probabilities'
  - name: 'Imandra Discover'
    notebookSlug: imandra-discover
  - name: 'Multifile development'
    notebookSlug: loading-files
  - name: 'Extracting OCaml modules'
    notebookSlug: extracting-ocaml-modules-with-imandra-extract
  - name: 'Code generation and plugins'
    notebookSlug: plugins
  - name: 'Imandra vs.'
    notebookSlug: imandravs
  - name: 'Imandra Python API'
    notebookSlug: python-api
  - name: 'Examples'
    notebookSlug: examples
    ignoreSubheadings: true
    miniSections: ['Beginner', 'Intermediate', 'Advanced']
    children:
    - notebookSlug: webservice-auth-logic
      name: 'Analysing Web-app authentication logic'
      miniSection : 'Beginner'
    - notebookSlug: simple-vehicle-controller
      name: 'Simple vehicle controller'
      miniSection : 'Beginner'
    - notebookSlug: simple-stoplight-model
      name: 'Simple car intersection model'
      miniSection : 'Beginner'
    - notebookSlug: singasong
      name: 'Rule Conflict Resolution'
      miniSection : 'Beginner'
    - notebookSlug: reasonml-tic-tac-toe
      name: 'Tic Tac Toe with ReasonML'
      miniSection : 'Beginner'
    - notebookSlug: reasonml-facetime-state-machines
      name: 'Exploring The Apple FaceTime Bug with ReasonML State Machines'
      miniSection : 'Beginner'
    - notebookSlug: crossing-river-safely
      name: 'Crossing the river safely'
      miniSection : 'Beginner'
    - notebookSlug: ubs-case-study
      name: 'Analysing the UBS ATS Dark Pool'
      miniSection : 'Intermediate'
    - notebookSlug: six-swiss-exchange-pricing
      name: 'Region Decomposition - Exchange Pricing'
      miniSection : 'Intermediate'
    - notebookSlug: verifying-an-ros-node
      name: 'Creating and Verifying a ROS Node'
      miniSection : 'Intermediate'
    - notebookSlug: key-pair-security
      name: 'Key Pair Security in Imandra'
      miniSection : 'Intermediate'
    - notebookSlug: sudoku
      name: 'Solving Sudoku with Imandra'
      miniSection : 'Intermediate'
    - notebookSlug: solver-synthesis
      name: 'Synthesising a game solver in Imandra'
      miniSection : 'Intermediate'
    - notebookSlug: exchange-implied-trading
      name: 'Exchange Implied Trading'
      miniSection : 'Intermediate'
    - notebookSlug: school-scheduler
      name: 'Solving school scheduling during COVID'
      miniSection : 'Intermediate'
    - notebookSlug: recursion-induction-and-rewriting
      name: 'Recursion, Induction and Rewriting'
      miniSection : 'Advanced'
    - notebookSlug: verifying-merge-sort
      name: 'Verifying merge sort in Imandra'
      miniSection : 'Advanced'
    - notebookSlug: ripple-carry-adder
      name: 'Verifying a Ripple Carry Adder'
      miniSection : 'Advanced'
    - notebookSlug: region-probabilities-example
      name: 'Calculating Region Probabilities'
      miniSection : 'Advanced'
    - notebookSlug: supervised-learning
      name: 'Analysing Machine Learning Models'
      miniSection : 'Advanced'
    - notebookSlug: probabilistic-reasoning-in-reasonml
      name: 'Probabilistic Reasoning in ReasonML'
      miniSection : 'Advanced'
    - notebookSlug: a-comparison-with-tla-plus
      name: 'A comparison with TLA+'
      miniSection : 'Advanced'
  - name: 'Reference'
    notebookSlug: reference
    children:
    - name: 'Standard Library'
      slug: odoc/imandra-base/Imandra_prelude/
    - name: 'OCaml API Docs'
      slug: odoc/
    - name: 'Python API Docs'
      slug: python/

sites-yaml: assets/jekyll-resources/_data/sites.yml

assets:
  template-paths:
    - templates/nbconvert
    - jekyll-resources
  hash-files:
    from-notebook:
      - static/style/style.min.css
      - static/custom/custom.css
      - static/nbextensions/nbimandra/styles.css
      - static/nbimandra-rjs-bundle.js
    from-assets:
      - static/docs-styles.css
      - static/jekyll-styles.css
      - static/jekyll-styles-dev.css
  folders:
    from-notebook:
      - static/components/font-awesome
    from-assets:
      - static/img
      - jekyll-resources/assets