rise4fun.com web page is down

[ftc]

I hope this is an appropriate place to post this. https://rise4fun.com has been down for the last two days. I have tried with different machines and different locations.

Work around:

The documentation is available on archive.org (without the online interpreter).

If someone is looking for a way to try Z3 without going through the build process, I am happy to upload a docker container with the latest version.

[NikolajBjorner]

It is pretty safe to assume that rise4fun will remain offline: the infrastructure used to build rise4fun is dated by about a decade and a complete overhaul would be required for rise4fun functionality to get it online with modern services and addressing any compliance issues.

Contributions for creating alternatives for using z3 install free (and maybe online) are highly welcome.

[ftc]

Thanks for letting me know about rise4fun. Its a shame since it is such a nice resource, but understandable that maintenance isn't easy.

I am happy to submit my docker image and scripts for z3 as a pull request if it looks helpful. But it duplicates some of what is already done for continuous integration in the contrib/ci directory.

I was able to compile Z3 to web assembly using this code and run it in a web browser. Unfortunately it isn't mine, but perhaps @bramvdbogaerde would be willing to contribute the code. Perhaps it would be easier to update rise4fun if it didn't require a back end?

[philzook58]

I'm sorry to hear that about rise4fun. It was extremely useful.
I've got a proof of concept of using the above mentioned wasm compiled version and hosting it as a static github.io website. This could be done from the Z3Prover organization's github.io website. https://philzook58.github.io/z3-wasm

[bramvdbogaerde]

I would be more than happy to contribute my scripts and glue code. However, it might be lacking as a full Z3 WASM solution as it leaves a lot of the Z3 C API unexposed. It should be sufficient for a rise4fun replacement though as it provides a way to evaluate SMT-Lib scripts.

I agree that a backend-free rise4fun replacement is preferable. In my opinion, a Github pages solution would be the best as it removes most dependencies on third parties which ensures the longevity of a rise4fun replacement.

[hzantema]

It is pretty safe to assume that rise4fun will remain offline: the infrastructure used to build rise4fun is dated by about a decade and a complete overhaul would be required for rise4fun functionality to get it online with modern services and addressing any compliance issues.

Contributions for creating alternatives for using z3 install free (and maybe online) are highly welcome.

https://compsys-tools.ens-lyon.fr/z3/index.php

is an alternative online z3 environment.

[NikolajBjorner]

Thanks for the input so far.

1. I have not followed developments on wasm bindings. Seems there are 3-4 independent variants. They appear to be of the form: invoke a specific build configuration to produce wasm, expose selected API functions, specifically parse_smtlib2_string.
   I wonder whether it makes sense to roll a general configuration into a an action or pipeline that can be built on releases, nightly or at merges. In the closest analogy I can think of, the Julia bindings uses the C++ API.
2. With emerging availability of code spaces one direction is to leverage this infrastructure. See TLA+ example https://github.dev/lemmy/ewd998 .

Thus, there are several different parts:

1. A wasm build process and binding support
2. Hosting z3 rise4fun pages (on GitHub pages) against local wasm run.
3. Leveraging GitHub code spaces for richer experiences.
4. Self-contained docker containers for stateful / wasm-less experiences

Some directions seem orthogonal. At any rate, quality contributions are gladly integrated or file github bugs to ensure z3 doc includes pointers to relevant external demos. While the benefits for sharing demos should be general interest, the required effort and quality level could go beyond weekend hobby level, so contact me directly about discussing support for self-contained work contract involving up to 80-100 hrs effort (probably only possible for US).

[philzook58]

That sounds very reasonable. I don't know much about the CI process, but I've been hobby tinkering further with my above demo based around z3-wasm which I've moved to https://philzook58.github.io/z3-rise4fun/ or https://www.philipzucker.com/z3-rise4fun/. It seems to largely be working other than the optimization and fixedpoint examples which don't work I assume because Z3_eval_smtlib2_string does not support their syntax.

Do you know if there is a copy of the rise4fun page that would have the fields in the "guide" that are marked "; click on edit to see the example"? The archive.org copy mentioned above does not have these contents available so far as i can tell.

[NikolajBjorner]

I am going to be digging up the sources for these pages. The ones that are on the cache have gone through a custom transformation that resolves some virtual links.

[NikolajBjorner]

Source tutorial files used for rise4fun are here: https://github.com/Z3Prover/doc/tree/master/riselive

[jfmc]

I've adapted @philzook58's Z3 rise4fun reconstruction with a monaco editor instance that includes very basic SMT2 syntax support. Probably a real front-end developer could do a much better job. Just in case someone finds it useful: https://jfmc.github.io/z3-play/

[NikolajBjorner]

amazing, it even works!

[philzook58]

Very slick! Nice!

[jfmc]

I'm glad it is useful!

I've pushed most of the code (I'm not proud of it but it should work) -- web branch for github pages and main branch for sources. I'll try to add github actions in the next days. To avoid duplications, I'd like to fetch the docs directly from https://github.com/Z3Prover/doc (it can be patched during z3-play build). My Z3->wasm build contains a few changes w.r.t. @philzook58 (basically disable some debug code so that the console/info output is cleaner). It would be awesome if Z3 provides official builds and interfaces (ala Lean browser builds and https://github.com/leanprover/lean-client-js).

[NikolajBjorner]

Links on https://github.com/Z3Prover/z3/wiki have been changed to z3-play.
I should likeley add other links.
Looking at optimization and fixedpoints. They don''t parse because the plugins are not loaded properly for the API supplied parser. For example: https://www.philipzucker.com/z3-rise4fun/optimization.html returns errors.
This should be fixable by ensuring that the plugins for optimization and fixedpoints get front loaded in the API parser.

[NikolajBjorner]

added ability to process opt and fixedpoint extensions, 3abecc3

[philzook58]

I have been able to compile Z3 wasm from master using the wasm.yml build script referenced below, but it didn't seem to fix the fixedpoint or opt behavior. They are still reported as unsupported

(get-info :version) 
(declare-rel a ())

(:version "4.8.14 - build hashcode 9e51691285d08cd7184bb6ad072c097431a49acc")
unsupported
; declare-rel line: 3 position: 17

For reference, this is the thin shim C code that takes an smtlib string and evaluates it in wasm. Perhaps the context needs to be set up differently for the extensions to work?

#include <z3.h>

static Z3_config config;
static Z3_context context;

void init_context() {
   config = Z3_mk_config();
   context = Z3_mk_context(config);
}

void destroy_context() {
   Z3_del_context(context);
   Z3_del_config(config);
   context = NULL;
   config = NULL;
}

const char* eval_smt2(char* input) {
   printf("Input %s\n", input);
   return Z3_eval_smtlib2_string(context, input);
}

[NikolajBjorner]

ouch. fixing....

[NikolajBjorner]

I pushed what should fix it

[philzook58]

Wow, thanks for the fast turnaround! This does appear to fix the fixedpoint and opt examples. I've pushed the updated z3 wasm binary to my github.io site. https://www.philipzucker.com/z3-rise4fun/fixedpoint.html

[stevegt]

@NikolajBjorner Do you still have control of the rise4fun domain, and if so would it be possible to set up a wildcard HTTP redirect pointing rise4fun.com/* queries to this page for the short term? If you want me to set up a redirect for you, I'd be happy to spin up a little container in our own environment that you can aim the A record at for the time being. I'm sure half the folks in this discussion would make the same offer and be happy to provide the support -- in my own case, an afternoon with Z3 has already helped me solve a problem I've been struggling with for years.

Here's why I think that redirect is important: As someone who only found Z3 a week ago, I've never seen rise4fun. But I've so far run into dozens of references to the site all over the Internet, in documents, blogs, stackoverflow answers, code comments, etc. In many cases, the reference is something along the lines of "here's a thing I'm going to mention in passing but am not going to explain, because this page over here at rise4fun documents it". And archive.org doesn't have many of those pages. For all I knew it's been down for years and nobody cared -- I didn't know what was going on until stumbling across this discussion just now.

[NikolajBjorner]

Microsoft owns that domain name. The server used for it is gone for good. Setting up redirects is a good suggestion. @pelikhan.

[NikolajBjorner]

@pelikhan - I am getting recurring questions about rise4fun domain being down. Can we perhaps redirect it to some github.io.rise web page where we can place links?

[NikolajBjorner]

A note for this thread is that since two weeks ago there is a GitHub Action that builds a WASM image.
https://github.com/Z3Prover/z3/actions/workflows/wasm.yml
I hope this can help with establishing a wasm image that is in sync with current state of z3.

[lwahonen]

That pipeline is producing a tar that contains a libz3.a, which doesn't smell like wasm (doesn't start with WASM_BINARY_MAGIC).

[lwahonen]

Weirdly https://github.com/Z3Prover/z3/actions/runs/1646912745 lists the file size at 102MB, but the actual download is just 25MB

[NikolajBjorner]

the zip file is "only" 25MB, the included tar-ball is 100MB.

[NikolajBjorner]

There is now an internship opportunity around RiSE for even more fun with z3 (and other tools) start date before July 1'st 2022.
Unfortunately, the internships are (still) remote and the constraints as far as I know are that
interns are residents in US or Canada by the time the offer is accepted.

This would allow us to host a well-maintained set of pages (that users run locally using wasm).
The idea is to further integrate, leverage, and extend, modern services (such as GitHub) with modern goodies
(an opportunity to go above and beyond with developer experiences).

https://careers.microsoft.com/us/en/job/1201362/Research-Intern-RiSE-Programming-Languages-Formal-Methods-High-Performance-Computing-Software-Engineering

[NikolajBjorner]

A wasm wrapper is now part of the repository with GitHub actions to build and registered in npm as z3-solver. #5762 thanks to Kevin Gibbons.
It is fairly comprehensive.