Skip to content

Commit

Permalink
added a playground for you to just run code
Browse files Browse the repository at this point in the history
  • Loading branch information
@ayanamonr
ayanamonr committed Jul 1, 2022
1 parent a5a8b23 commit 663a786
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 0 deletions.
10 changes: 10 additions & 0 deletions website/docs/playground/playground.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
---
title: Playground
sidebar_position: 1
---

Run Z3 Code on the web!

```z3
(echo "Type here and press render to run your z3 code")
```
6 changes: 6 additions & 0 deletions website/docusaurus.config.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,12 @@ async function createConfig() {
position: 'left',
label: 'Strategies',
},
{
type: 'doc',
docId: 'playground/playground',
position: 'left',
label: 'Strategies',

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner Jul 1, 2022

Collaborator

wrong label
},
// link to the github repo of this site
{
href: 'https://github.com/microsoft/rise4fun',
Expand Down

3 comments on commit 663a786

@NikolajBjorner
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is awesome!

It is taking exciting shape.

I am finding a bunch of details to look after. Many are around z3 behavior that I have to figure out.
There are some cases of where the z3 environment is used for code snippets that are not runnable. I removed the z3 tag from some of these examples, but new material contains more instances.
I will be iterating on the technical part of the content in the coming days, so it is in even better shape to show.
Whatever you find some typos or other details make sure to fix them.
The build generates error messages. I haven't figured out to streamline the process of taking error messages and go through examples to fix them so at this point it is a brute force.
On editorial content, I think we want to figure out how to integrate pointers to the reference material (z3prover.github.io) and make space for (1) programming z3 style material, (2) python tutorials, if we get them on par with the JS (3) case studies / fun examples. The top horizontal bar gives a good way to navigate main sections.

@pelikhan
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rlisahuang you need to support a way to tell the remark build to ignore a z3 snippet. Something like this:

```z3 no-build
This snippet won't build
```

and also another one to completely ignore errors (maybe you are teaching about syntax errors)

```z3 ignore-errors
Code that has errors but we don't care
```

@pelikhan
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The build generates error messages. I haven't figured out to streamline the process of taking error messages and go through examples to fix them so at this point it is a brute force.

@rlisahuang One way to simplify finding each snippet that has a problem is to generate a logging error message that is compatible with the github action annotations --> https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-a-warning-message

Please sign in to comment.