microsoft / z3guide

Tutorials and courses for Z3
https://microsoft.github.io/z3guide
MIT License
62 stars 23 forks source link

Z3Guide Documentation

This repository contains sources of Z3Guide, an online tutorial for Z3 powered by RiSE at Microsoft Research.

The rest of this page is for developers contributing to the tutorial docs of Z3.

Table of Content

  1. Developer Setup
    1. Local Setup
    2. Codespaces
  2. Development
    1. Contributing to Existing Materials
    2. Creating New Tutorial Materials
    3. Testing the Website
  3. Manually Updating z3-solver
  4. Code of Conduct
  5. Trademarks

Developer Setup

Local Setup (not using Codespaces)

npm install -g yarn

Codespaces

These instruction use GitHub Codespaces, a convienient way to get a perfect cloud development environment. Your organization may or may not support Codespaces.

Microsoft Employees ONLY

Development

cd website
yarn
yarn clear; # for clearing cache
yarn start; 

Inspecting the Output from the Build

yarn clear; # clearing your cache first is always recommended
yarn build;

and if successful, you should see a build directory under website.

The online Z3 Guide serves multiple instances of tutorial materials: currently it has a Z3 tutorial in SMTLIB format, and Programming Z3 in different language bindings.

The instances are hosted under website/docs-smtlib and website/docs-programming, respectively. To contribute to existing tutorial materials, you may add/edit materials in either directory.

Creating New Tutorial Materials

The process of creating new tutorial materials is similar to the above, except for the following additional steps:

  1. You will need to create a new docs-* directory under website. E.g., website/docs-api.
  2. You will need a JavaScript file for configuring the sidebar for your docs under website/sidebars. The sidebar can be generated automatically. You may simply make a renamed copy of programmingSidebars.js for such automation.
  3. You will need to go to docusaurus.config.js to add additional configurations so that the build process can pick up the new directories. Search for comments beginning with [NEW DOCS] within the file for more instructions.

Testing the Website

We provided a test file that contains all kinds of Z3 (SMTLIB and JavaScript) code snippets, docs-playground/_03.test.md. To test if the interactivity with Z3 snippets works as expected, you may remove the underscord at the beginning of the file name, and run

yarn start

to access the file at https://localhost:[PORT]/z3guide/playground/test, where [PORT] is 3000 by default or the port number you specified in docusaurus.config.js.

You may add more code snippets to this test file, or create your own test file under any docs-* directory your prefer. We recommend putting the test files under docs-playground.

When you are done testing, make sure to add the underscore back to the test file name, so that the content will not be included in rendering the website.

Manually Updating z3-solver

Upgrades of z3-solver should be done ONLY you are certain that the latest version of z3-solver works well with the existing examples and website infrastructure. We provide a script to automate the manual upgrade process:

# remember to switch into the `website` directory first
yarn upgrade-z3

The script will update z3-solver to the latest and then try to build the website. If the build fails, then it will downgrade z3-solver to the version before your upgrade. It is unlikely that the update itself fails.

After done, make sure the field dependencies.z3-solver in website/package.json is exactly the version that you just upgraded to. For example, if you just upgraded to version 4.10.1, it should look like

{
  //...
  "dependencies": {
    //...
    "z3-solver": "4.10.1" // it should not be "^4.10.1" or "~4.10.1" or any other values that contain other symbols
  }
}

So that we make sure that yarn install always picks up the exact version of z3-solver that you mean for the website to run on.

Microsoft Open Source Code of Conduct

This project is hosted at https://github.com/microsoft/z3guide/. This project has adopted the Microsoft Open Source Code of Conduct.

Resources:

Trademarks

This project may contain trademarks or logos for projects, products, or services. Authorized use of Microsoft trademarks or logos is subject to and must follow Microsoft's Trademark & Brand Guidelines. Use of Microsoft trademarks or logos in modified versions of this project must not cause confusion or imply Microsoft sponsorship. Any use of third-party trademarks or logos are subject to those third-party's policies.