This is a multi-agent prototype to show a market modeled in Soda.
Steps to run the example :
- To run these steps, you need to install:
- Get the Soda translator binary by either doing the following:
- a. download the Linux binary from releases
- b. or clone the Soda repository and compile it, by either:
- i. run the
makeall.sh
, from a Linux compatible environment - ii. or run
sbt
to get an executable JAR file as indicated in the Soda release notes. The command itself is described inbuild
and the file isrelease
. To execute a JAR file, you need a Java environment installed, and you need to runjava -jar filename.jar
, for a JAR file namedfilename.jar
.
- i. run the
- c. make sure that the binary file
soda
is reachable from the command line, for example by updating the environment variablePATH
.
- Once you got the binary translator, go to an empty directory and try
soda manual
. It will output a piece of code with many examples, but most importantly, this mini-manual is a "Hello, World!" program itself. Writesoda manual > Manual.soda
and you get the manual. - To compile this project, run
makeall.sh
, from a Bash terminal. It creates a file namedmarket
and copies the exampleexample0.yaml
to the project root directory. - Try running
market example0.yaml
, and modify its values, to test how it works. The supported operations are:- deposit user amount : declare a user account if necessary, and put money into the account;
- assign item user : declare an item if necessary, and define its owner;
- price item amount : define the price of an item, or hide it if its price is 0;
- sell item user : exchange an item and its price between a buyer and a seller.
- To translate the Soda files into Scala and Lean, and then compile the Lean files, run
update.sh
. - You can edit the Soda files with IntelliJ and compile them with the
soda
binary. - You can see and verify the Lean translations with Visual Studio Code. The translated files are in directory Soda, and in particular the package core.
Soda is a functional language intended to be easy to learn and to read. However, writing purely functional style requires some practice, as some things are different from the imperative style. In addition, Soda includes an object-oriented notation to align it with mainstream object-oriented programming languages, and to make its notation familiar to users acquainted to those languages. For more details about Soda, see the Soda manual.
To get familiar with the verification possibilities, a good way to start proving theorems in Lean is to follow the tutorials at the Lean Game Server, like the Natural Number Game.
The project can be built with sbt with
sbt clean compile test package assembly
A Linux binary can be created with the script makeall.sh
.
More detailed information can be found in the release notes.