microsoft / z3guide Goto Github PK

• Ensure that if a snippet cannot be processed during build, the entire github action fails as well (and no deployment is generated).
• Ensure that logging is good enough to trace which snippet needs to be investigated. Try to generate an formatted error message in the output so that the github action automatically highlights where the problem is

#7

rehype-sanitize might be useful

ensure that the content is properly handled by a screen reader, in particular that changes to the output div are properly announced (use something like aria-live)

• get familiar with how to theme
• presentable!

create a new logo for the site and for potential "merch" and such

https://www.figma.com/file/8DIxJUBYNPj9AqOxifgoPQ/Z3-Designs?node-id=0%3A1

• big title at start should probably have some other content
• learn z3 at bottom section is somewhat misleading as it takes the user to another web site. suggestion: remove

Currently thinking about the design from https://infinum.github.io/eightshift-docs/, minus the sections below intro. So just one big background, a big title, some text description, and two buttons that get you to Tutorial and Playground, respectively.

It should be able to be done through pure CSS.

TODOs:

• background pic?
• landing page redesign
• theme color? thinking about blu-ish due to the current Z3 logo
• @NikolajBjorner Z3 logo in SVG/PNG?

• take z3 snippets from the native cli -> into remark tree
  • z3 cli in codespace -> talk to nbjorner ( about the npm stuff )
  • create a remark package that grabs z3 snippets runs and injects output
  • caching mechanism locally
  • ? what happens when z3 fails ?
  • ? how many clis at once ? -> to start one, think about how to do more
  • configure ghactions to leverage the cache mechanism across builds

Example of commit messages:
feature:semantic-release or major:semantic-release

• set up docusaurus
• build in github action
  • check that the typescript stuff works
• deploy to ghpages

• In all website/docs/*.md files, change all instances of

```
<some code>
```

to

```z3
<some code>
```

• There are some missing quotation marks for strings and angle brackets for int comparisons in the material currently in docs/intro.md. Please fix those manually. For example:

(echo starting Z3...) ;; missing quotations around "starting Z3..."

and

(assert ( a 10)) ;; should have been `(assert (> a 10))`

Missing wrap and copy buttons.

using github action/cache to cache pre-computed z3 runs in build

Having the version number on the website somewhere (at least on the playground) would be helpful for users who run into bugs and want to report them.

• enable katex to render the math necessary

#7

• Check existing Remark plugins vs. write our own

• make sure instructions for this step is clear for a user (subject b)
• note: content in a subfolder
• make sure everything in codespace is installed on launch
• instruction on dev server launch should be clear
• !!! as we hear about what professors need edit

• Add interactivity with Z3 (SMT-LIB)
• Migrate content from the Python tutorial and have the Z3 Python bindings run in the browser (maybe through Pyodide?)
• Z3 JS content
• Improve content through interviews

• convert html content to markdown
• split content into different files

This example shows no output in pre-built mode:

The (set-logic HORN) seems not to be respected from Z3_eval_smtlib2_string.

Ensure that the page can be navigated with a keyboard, specifically that the interactive snippet editor can be keyboard operated (add short cuts for run, make sure one can escape from the snippet)

For changes not in website/docs:

• use short-lived branches and do micro-commits incrementally
• when done, open a PR so that the automated build can run (to see if pass/fail as a self check)
• if satisfied, merge the PR into main and delete the temporary branch

describe record update construct for algebraic datatypes

Develop schema for cross referencing material from the tutorial.
So far there is a way to cross reference SMTLIB in some format. For example.

SMTLIB2 standard Integers

Other categories of cross references are:

• Reference manual
• Lectures
• Papers
• Case Studies
• Stackoverflow questions / github discussions - in a nutshell user interaction.

What is a good schema for the static content and way to integrate dynamic content?
Preliminary way:

[!TIP]
Optional information to help a user be more successful.

[!IMPORTANT]
Essential information required for user success.

[!CAUTION]
Negative potential consequences of an action.

[!WARNING]
Dangerous certain consequences of an action.

The last point about cross-referencing user interaction is more ambitious and should be aligned with developing methods to integrate learning feedback. Given the state of z3guide, what is the long- and short-term plan for integrating such signals?
What are the technical enablers? (let me zoogl3 this, or link to github discussions, create discussions, cross-link discussions?)

Once a snippet is edited, add button to reset to original code

Now that we eval every z3-js snippet, the door to potential security attacks is opened.

A possible scenario I could think of is that someone forks this repo, changes some z3-js content to be malicious, and hosts it on a public github page. Visitors of that page could have their information stolen through such malicious content.

Pretty sure the official docusaurus website has some mechanism against it as there are executable and editable JS blocks too.

TODO:

• look into sandboxing / sanity checks that the built-in editor might provide.

Click the first "discuss" button at https://microsoft.github.io/z3guide/programming/Z3%20from%20Python/advanced

(notice URL)

There are several issues with the top-level organization.

• The top-level organization shows z3 topics on the main landing page. The z3 topics should (eventually?) only show up when selecting the z3 tutorial (reflecting that rise4fun is more than z3 even though current activities are z3 centric).
• When selecting the z3 tutorial the page is undefined. What is the right link? Where should it be added?
• The side bar shows z3 sections in an indeterminate order. The order in the upper task bar is according to a json file, but the order in the left side bar is neither logical, nor alphabetical.

Attempting to run Z3 in the browser (currently without webworkers). Code in #42 .

According to @NikolajBjorner it seems that there have been major changes to the JS API since June 14, which involves the names of several files (e.g. wrapper.js was gone) and the signature of init (it used to accept one argument, which is the result of initZ3, now none).

@bakkot It would be super helpful if you could provide us with some examples of:

• Running Z3 in the browser without webworkers, and
• ... using webworkers

with the current (4.9.1) npm release.

Currently the reference documentation is built on releases and available as a zip file from the release hive.

https://github.com/Z3Prover/z3/releases/download/z3-4.9.1/z3doc.zip

Then I manually download this and unzip the contents into z3prover.github.io/api/html
It is a repository under https://github.com/z3prover
Commit and push

The process for uploading artifacts should be reasonably similar for releases.
Even a self-contained GitHub action that builds documentation by itself and pushes to the right place (could be microsoft.github.io/z3guide if this is better) would be great and perhaps easier to maintain than complicating the release.yml Azure pipeline.

https://github.com/microsoft/rise4fun/blob/e51230ced0d0a6f5b5a174232701bf57c0e63983/website/docs/05%20-%20Arithmetic/_category_.json#L6

Once the SMTLIB tutorial is interactive, the format of the site may very well transition to a wider scope.
The indexing used here
https://github.com/facebook/docusaurus/blob/main/website/docusaurus.config.js
allows for multiple sections.

For z3 the main sections are:

• Z3 Tutorial (SMTLIB):
  • Logic
  • Theories
  • Strategies
  • Fixedpoints
  • Optimization
  • Playground
• Programming Z3 Tutorial:
  • Interface concepts (a section that explains main interface concepts and their behavior. Examples in Python?)
    • Context
    • Expressions, Sorts, Functions
    • Model
    • Solver
    • Optimize
    • Fixedpoints
    • Tactic
  • Guides
    • Python tutorial
    • programmingz3 document
  • Examples/Case studies
    • point to examples from GitHub
    • interactive examples (in Python)
    • external links
    • Bazar
• Language Binding reference (currently at https://z3prover.github.io/api/html)
  • C
  • C++
  • Python
  • Dotnet
  • Java
  • OCaml
  • JS

Other notes:

• Java Script Tutorial (maybe, or mesh with SMTLIB Tutorial).
• Python Tutorial (import Jupyter notebooks and programmingz3.mdk)
• API (link to z3prover.github.io/api/html, or automatically pull material from doc.zip on release)
• Examples/Case Studies/Home work - some format for sharing information and adding content.
• External resources:
  • There are external resources (generally, I have little idea and they just appear out of nowhere, but they seem to be known to students): Rust API, Haskell API, PySMT, ...
• Reference material:
  • programming z3 - that is, using z3 to program constraint solving services.
  • z3 internals - planned for January tutorial, a tutorial introduction on algorithms and implementation for SMT

Resources, such as Slides are linked at bottom of page.

• github button linking to a main github discussion thread for the online guide?
• same thing for stackoverflow? (some work that Denae Ford has worked on?)
• emailing the professor?
• line numbers?
• copy button?
• reset button?
• keyboard navigation?

The tutorial should link with a slide share.
At this point https://z3prover.github.io/slides.
The directory is not indexed so currently have to know names of slides "tuv22.html" and "q.html" and "setts.html"
Sources are: https://github.com/z3prover/ (under z3prover.github.io).

Avoid inline html as possible

Use (dreaded) markdown syntax for tables

• integrate also other tutotiral material

  • the "advanced", "tactic", "fixedpoint" guides. @ayanamonr
  • Collect material on "optimize" and create a tutorial for it. @NikolajBjorner
  • Add tutorial material on seq and regex @NikolajBjorner
  • Add tutorial material on special relations @NikolajBjorner
  • Add tutorial material on algebraic datatypes + arrays + sequences @NikolajBjorner

• integrate tutorial material based on case studies, such as:

  • z3 "the wedding planner" @ayanamonr and Aidan from CMU
  • z3 "for tax planning". @NikolajBjorner

• have a way to assemble pointers to other self-contained examples. A static set of links could bit-rot. Is there a good dynamic approach (let me zoggl3 that for you?)

• assemble and allow for adding links to youtube material.

  • Nadia has a 30 minute tutorial where she uses the python API. The python code is stored in a Git repository. Can we link to such videos and make the reproducibility of such tutorial easier than just dumping files in a Git?

• add a mode for running Java script examples

  • add tag z3js similar to z3 tag for environments.
  • it runs the java script in the enclosure together with suitable imports.
  • then one can mix java script examples with the smtlib2 examples

• run python code samples

  • can we use something like Pyodide as used here https://pysathq.github.io/

• integration with documentation generation.

  • https://www.doxygen.nl/manual/markdown.html
  • https://stackoverflow.com/questions/13081984/generate-documentation-as-markdown-files-using-doxygen

Overall:

• how do we best integrate cross referencing?
  • Started to add cross reference to SMTLIB2 documentation. ad hoc
  • Cross reference to examples
  • Cross reference to reference documentation
  • Cross reference to github discussions and stackoverflow discussions or other discussions
• how can the tutorial and learning material be made palatable for contributors?
  • Some users could be tempted to add example material (puzzle solving) and making it easier to add such helps everybody.

Several code snippets from our tutorial would not work in the web interface cited above. According to @NikolajBjorner z3-wasm does produce different outputs than the z3 executables.

Code snippet example:

(set-option :print-success true) 
(set-option :produce-unsat-cores true) ; enable generation of unsat cores
(set-option :produce-models true) ; enable model generation
(set-option :produce-proofs true) ; enable proof generation
(declare-const x Int)
(set-option :produce-proofs false) ; error, cannot change this option after a declaration or assertion
(echo "before reset")
(reset)
(set-option :produce-proofs false) ; ok

Moving the conversation from #19 .

The possible solutions we face:

1. Remove tutorial materials that contain such problems;
2. Coordinate with @NikolajBjorner and @bakkot on a wasm build that produces consistent outputs.

The second argumen of visit should be a logger; we should use that in order to get proper logging in the builds

It would be more efficient to immediately show the pre-computed output (that's one less button and it's useful information). We have it let's show it.

I recommend doing this in remark at rendering time by generating a new code node; that later gets rendered by docusaurus. As a bonus, it should be the copy/wrap icons.

Also, drop "Output:", it feels more like noise at this point.

• static website > docusaurus < @rlisahuang
• migrate content to markdown @ayanamonr
• katex enabled for the math stuff @rlisahuang
• native computing every snippet at runtime @rlisahuang
• github publish action
  • make sure the typescript stuff is correctly
• codespace configured
• bjorner onboarding documentation @ayanamonr << last step! Subject B :)
• react component to render output

• add a button next to Run that links to the Z3 github discussion page

• renders z3 source on output

https://github.com/microsoft/rise4fun/blob/e51230ced0d0a6f5b5a174232701bf57c0e63983/website/docs/02%20-%20basic-commands/02%20-%20using-scopes.md?plain=1#L2

Move all remark plugin settings to configuration

• timeout duration
• executable name and argument format
• tool name (eg. z3)
• custom version number to force hash recomputation

The settings should allow to run the remark tool against another command line tool --> support an array of tool descriptions.

• a. Forking this website to extend / customize the existing z3 guide and host on the user's own github pages;
• b. Forking the tutorial template to customize an online tutorial for a custom language

Context

I encountered some issues with getting the TypeScript bindings to work in Node.js. The idea is to break down a given code snippet (in the smt2 format) by line and obtain the output through Z3.eval_smtlib2_string. My main reference is this z3-wasm webpage, which uses our official WASM build. The way inputs are processed is detailed in their main.js file.

Problem with Node.js

Note that this website runs z3-wasm in the browser from the client side, while we want to run z3-wasm with Node.js from the server side. Therefore, their logic for running Z3 does not work in our scenario -- I had RuntimeErrors complaining about the inability to find z3-built.wasm. My implementation for running Z3 (currently commented out) can be found in website/src/remark/render-code-blocks.mjs in PR #18 .

Additional issue(s) with z3-wasm

I also noticed that several code snippets from our tutorial would not work in the web interface cited above. I wonder if this is a bug with the WASM build, or if there are additional API calls we should use instead for such code snippets. An example of snippet that does not work in the web interface:

(set-option print-success true) 
(set-option produce-unsat-cores true) ; enable generation of unsat cores
(set-option produce-models true) ; enable model generation
(set-option produce-proofs true) ; enable proof generation
(declare-const x Int)
(set-option produce-proofs false) ; error, cannot change this option after a declaration or assertion
(echo before reset)
(reset)
(set-option produce-proofs false) ; ok

I got a bunch of syntax errors when I ran it in that web interface.

@NikolajBjorner We would like some help from Kevin on the following issues:

1. A simple example of running z3-wasm in Node.js with smt2-formatted inputs;
2. The syntax errors I got from running code snippets from our tutorial in the existing web interface -- is it a bug, or are there ways around it?

• From the Python guide
• From the high-level API unit test: https://github.com/Z3Prover/z3/blob/master/src/api/js/src/high-level/high-level.test.ts

There is a new release of z3 out today.
It doesn't seem to get picked up by the build.
It has some npm version dependencies as well that have changed.
With this release we should be able to remove some of the no-build tags.