emina / rosette

The Rosette solver-aided host language, sample solver-aided DSLs, and demos
Other
638 stars 74 forks source link

Is there a simple 4.0 syntax for with-asserts/with-asserts-only? #200

Closed kwmaeng91 closed 3 years ago

kwmaeng91 commented 3 years ago

Hi, I am new to Rosette. I am relying on many old resources from the web to learn it. However, many are from the incompatible 3.x version and the examples they have are not compatible with 4.0. So I was wondering if there are simple one-to-one translations from the removed syntax, e.g., with-asserts/with-asserts-only, to new syntax, e.g., with-vc. with-vc looked close enough, but since I cannot find what with-asserts/with-asserts-only was supposed to be doing (because I cannot find the relevant doc for 3.x anymore), I am not even sure if replacing them with, e.g., with-vc, makes sense. Is there a simple translation from those deprecated 3.x syntax to the new 4.0 syntax? Or is there any old document I can look into to understand what those "old" syntaxes are doing to understand old Rosette codes?

Let me know if this is not a proper place for general questions (and in that case, if you can guide me to a proper channel I would really appreciate it).

Thank you.

emina commented 3 years ago

Hi! The translation from Rosette 4 to Rosette 3 is not quite 1-1. But as a rough guideline, all code that used with-asserts/with-asserts-only can be (re)written using with-vc. If there are some specific examples we can help with, let us know.

To help with the transition from Rosette 3 to Rosette 4, you can build the documentation for Rosette 3 locally as follows (tested on a Mac):

# Temporarily uninstall Rosette 4:
$ raco pkg remove rosette

# Check out the Rosette repo and switch to the 3.2 tag: 
$ git clone git@github.com:emina/rosette.git rosette3
$ cd rosette3
$ git fetch --all --tags
$ git checkout tags/3.2

# Install Rosette 3.2 from source, which builds the Rosette 3 documentation. 
$ raco pkg install --name rosette
$ open rosette/doc/rosette-guide/index.html

# Uninstall Rosette 3 and install Rosette 4 again from the Racket server:
$ raco pkg remove rosette
$ raco pkg install rosette
sorawee commented 3 years ago

-D in raco pkg install -D --name rosette means no docs, so I think it should be left out? I.e., raco pkg install --name rosette

Also, in case the documentation is not at rosette/doc/rosette-guide/index.html (mine is not). you can use raco docs rosette to open up the documentation too.

sorawee commented 3 years ago

I just noticed that you are Kiwan that posted the question about Rosette 3 installation in the Racket mailing list, right? If you already have Rosette 3 installed, I think you can use raco docs rosette to find the documentation right away.

emina commented 3 years ago

-D in raco pkg install -D --name rosette means no docs, so I think it should be left out? I.e., raco pkg install --name rosette

Yes, good catch, fixed the instructions.

kwmaeng91 commented 3 years ago

Thank you both for the help! Like @sorawee noticed, I am just using Rosette 3.x for now which I got with raco. Unfortunately, I did not install the doc (because I have very little disk space :P) when I installed Rosette 3, but I will maybe re-install it later with the doc.