microsoft/z3guide

microsoft/z3guide

Description: Tutorials and courses for Z3

Language: JavaScript

License: MIT

Stars: 109

Forks: 32

Open issues: 16

Created: 2022-06-13T17:34:04Z

Pushed: 2026-06-09T22:55:56Z

Default branch: main

Fork: no

Archived: no

README:

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](#developer-setup) 1. [Local Setup](#local-setup-not-using-codespaces) 2. [Codespaces](#codespaces-microsoft-internal-only) 2. [Development](#development) 1. [Contributing to Existing Materials](#contributing-to-existing-tutorial-materials) 2. [Creating New Tutorial Materials](#creating-new-tutorial-materials) 3. [Testing the Website](#testing-the-website) 3. [Manually Updating z3-solver](#manually-updating-z3-solver) 4. [Code of Conduct](#microsoft-open-source-code-of-conduct) 5. [Trademarks](#trademarks)

Developer Setup

Local Setup (not using Codespaces)

• install node.js >= 20
• install yarn globally if needed

npm install -g yarn

• Set up repo and start development following the steps in [Development](#development).

Codespaces

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

• From this repository, click on the green <> Code button, select the Codespaces tab and then Create codespaces on main. The setup might take a couple of minutes.

• From there, a VSCode tab will open in your browser. You may now edit, test and commit to the repository just like on your local machine.

• All command line instructions assume a bash-like terminal.

• Set up repo and start development following the steps in [Development](#development).

Microsoft Employees ONLY

• Join the Microsoft github organization from Microsoft Open Source via the Employee sign-in at the bottom.

• From there, go to the GitHub for Open Source at Microsoft tab and follow the instructions to join the organization via the management portal.

Development

• Change the working directory to website:

cd website

• From website, run the script to install dependencies

yarn

• Launch the docs server (which does client-side rendering and allows for hot reloading, so that you see your changes immediately reflected to the locally running page)

yarn clear; # for clearing cache
yarn start;

• Click on the generated URL in the terminal output to see the website now running locally.

Inspecting the Output from the Build

• In case you want to inspect the output (.html files etc. from server-side rendering) from the build, you can run

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

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

• If you want to see how these output files are rendered in the browser, you may run

yarn serve

Note that this is _different_ from yarn start, as yarn serve does not do hot-reloading because it is simply _serving_ the files under build rather than rebuilding everything from scratch for every change you make, like what yarn start does.

Contributing to Existing Tutorial Materials

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.

• You may find the Docusaurus documentation on Docs useful, especially for configuring the sidebar.

• Note that Docusaurus does live reload, so that every change you make to website/docs will be immediately reflected in the locally running tab.

• For all Z3-SMTLIB code snippets, please use the following Markdown code blocks format:

~~~

(exec-this-command arg)

~~~

• Any Z3 runtime error with the code specified in the code block above would fail the build.

However, you may intentionally bypass the errors by using flags of no-build or ignore-errors:

~~~

give me the error on the webpage I know it is invalid

~~~

or ~~~

I know this snippet is problematic but I want to teach about error messages so show them

~~~

• You may also add Z3-JavaScript or Z3-Python code snippets using Markdown code blocks, e.g.,:

~~~

// some z3-js code

~~~

and

~~~

# some z3-python code

~~~

and the flags of no-build and ignore-errors remain applicable to these code blocks.

Note that we currently support output rendering and code editing for Z3-SMTLIB and Z3-JavaScript code snippets, with similar support for Z3-Python coming soon.

• Programming Z3 in other language bindings is not supported at the moment.

• Sidebar content is maintained in files under website/sidebars. The Z3-SMTLIB guide uses website/sidebars/smtlibSidebars.js, while the Programming Z3 (with other language bindings) guide uses website/sidebars/programmingSidebars.js. If you find your new content missing from either sidebar, please modify the respective sidebar file accordingly.

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…