Commit 7757e086 authored by Dario Pinto's avatar Dario Pinto
Browse files

Merge branch 'master' into 'master'

two last articles

See merge request OCamlPro/www!75
parents 24ff235f 2ba56761
title=Release of Alt-Ergo 2.4.0
authors=Albin Coquereau
date=2021-01-22
category=Formal Methods
tags=alt-ergo
A new release of Alt-Ergo (version 2.4.0) is available.
You can get it from [Alt-Ergo's website](https://alt-ergo.ocamlpro.com/). The associated opam package will be published in the next few days.
This release contains some major novelties:
- Alt-Ergo supports incremental commands (push/pop) from the [smt-lib ](https://smtlib.cs.uiowa.edu/)standard.
- We switched command line parsing to use [cmdliner](https://erratique.ch/software/cmdliner). You will need to use `--<option name>` instead of `-<option name>`. Some options have also been renamed, see the manpage or the documentation.
- We improved the online documentation of your solver, available [here](https://ocamlpro.github.io/alt-ergo/).
This release also contains some minor novelties:
- `.mlw` and `.why` extension are depreciated, the use of `.ae` extension is advised.
- Add `--input` (resp `--output`) option to manually set the input (resp output) file format
- Add `--pretty-output` option to add better debug formatting and to add colors
- Add exponentiation operation, `**` in native Alt-Ergo syntax. The operator is fully interpreted when applied to constants
- Fix `--steps-count` and improve the way steps are counted (AdaCore contribution)
- Add `--instantiation-heuristic` option that can enable lighter or heavier instantiation
- Reduce the instantiation context (considered foralls / exists) in CDCL-Tableaux to better mimic the Tableaux-like SAT solver
- Multiple bugfixes
The full list of changes is available [here](https://ocamlpro.github.io/alt-ergo/About/changes.html). As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!
title=New Try-Alt-Ergo
authors=Albin Coquereau
date=2021-03-29
category=Formal Methods
tags=alt-ergo
![](/blog/assets/img/screenshot_ask_altergo.jpg)
Have you heard about our [Try-Alt-Ergo](https://alt-ergo.ocamlpro.com/try.html) website? Created in 2014 (see [our blogpost](https://www.ocamlpro.com/2014/07/15/try-alt-ergo-in-your-browser/)), the first objective was to facilitate access to our performant SMT Solver [Alt-Ergo](https://alt-ergo.ocamlpro.com/). *Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.*
This playground website has been maintained by OCamlPro for many years, and it's high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the [Try-Alt-Ergo](https://try-alt-ergo.ocamlpro.com/) website! In this article, we will first explain what has changed in the back end, and what you can use if you are interested in running your own version of Alt-Ergo on a website, or in an application! And then we will focus on the new front-end of our website, from its interface to its features through its tutorial about the program.* *
## [Try-Alt-Ergo 2014](https://www.ocamlpro.com/2021/03/29/new-try-alt-ergo/#2014)
![](/blog/assets/img/screenshot_from_2021_03_29.png)
[Try-Alt-Ergo](https://alt-ergo.ocamlpro.com/try.html) was designed to be a powerful and simple tool to use. Its interface was minimalist. It offered three panels, one panel (left) with a text area containing the problem to prove. The centered panel was composed of a button to run Alt-Ergo, load examples, set options. The right panel showed these options, examples and other information. This design lacked some features that have been added to our solver through the years. Features such as models (counter-examples), unsat-core, more options and debug information was missing in this version.
Try-Alt-Ergo did not offer a proper editor (with syntax coloration), a way to save the file problem nor an option to limit the run of the solver with a time limit. Another issue was about the thread. When the solver was called the webpage froze, that behavior was problematic in case of the long run because there was no way to stop the solver.
## [Alt-Ergo 1.30](https://www.ocamlpro.com/2021/03/29/new-try-alt-ergo/#ae-1.30)
The 1.30 version of Alt-Ergo was the version used in the back-end to prove problems. Since this version, a lot of improvements have been done in Alt-Ergo. To learn more about these improvements, see our [changelog](https://ocamlpro.github.io/alt-ergo/About/changes.html) in the documentation.
Over the years we encountered some difficulties to update the Alt-Ergo version used in Try-Alt-Ergo. We used [Js_of_ocaml](https://ocsigen.org/js_of_ocaml/latest/manual/overview) to compile the OCaml code of our solver to be runnable as a JavaScript code. Some libraries were not available in JavaScript and we needed to manually disable them. The lack of automatism leads to a lack of time to update the JavaScript version of Alt-Ergo in Try-Alt-Ergo.
In 2019 we switched our build system to [dune](https://dune.readthedocs.io/en/latest/overview.html) which opens the possibility to ease the cross-compilation of Alt-Ergo in JavaScript.
## [New back-end](https://www.ocamlpro.com/2021/03/29/new-try-alt-ergo/#backend)
With some simple modification, we were able to compile Alt-Ergo in JavaScript. This modification is simple enough that this process is now automated in our continuous integration. This will enable us to easily provide a JavaScript version of our Solver for each future version.
Two ways of using our solver in JavaScript are available:
- `alt-ergo.js`, a JavaScript version of the Alt-Ergo CLI. It can be runned with `node`: `node alt-ergo.js <options> <file>`. Note that this code is slower than the natively compiled CLI of Alt-Ergo.In our effort to open the SMT world to more people, an npm package is the next steps of this work.
- `alt-ergo-worker.js`, a web worker of Alt-Ergo. This web worker needs JSON file to input file problem, options into Alt-Ergo and to returns its answers:
- Options are sent as a list of couple *name:value* like:`{"debug":true,"input_format":"Native","steps_bound":100,"sat_solver": "Tableaux","file":"test-file"}`You can specify all options used in Alt-Ergo. If some options are missing, the worker uses the default value for these options. For example, if debug is not specified the worker will use its defaults *value :false*.- Input file is sent as a list of string, with the following format:`{ "content": [ "goal g: true"] }`
- Alt-Ergo answers can be composed with its results, debug information, errors, warnings …`{ "results": [ "File \"test-file\", line 1, characters 9-13: Valid (0.2070) (0 steps) (goal g) ] ,``"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver"] }`like the options, a result value like `debugs` does not contains anything, `"debugs": [...]` is not returned.
- See the Alt-Ergo [web-worker documentation](https://ocamlpro.github.io/alt-ergo/Usage/index.html#js-worker) to learn more on how to use it.
## [New Front-end](https://www.ocamlpro.com/2021/03/29/new-try-alt-ergo/#frontend)
![](/blog/assets/img/screenshot_new_altergo_interface.jpg)
The [Try-Alt-Ergo](https://try-alt-ergo.ocamlpro.com) has been completely reworked and we added some features:
- The left panel is still composed in an editor and answers area
- [Ace editor](https://ace.c9.io/) with custom syntax coloration (both native and smt-lib2) is now used to make it more pleasant to write your problems.
- A top panel that contains the following buttons:
- `Ask Alt-Ergo` which retrieves content from the editor and options, launch the web worker and print answers in the defined areas.
- `Load` and `Save` files.
- `Documentation`, that sends users to the newly added [native syntax documentation](https://ocamlpro.github.io/alt-ergo/Input_file_formats/Native/index.html) of Alt-Ergo.
- `Tutorial`, that opens an interactive [tutorial](https://try-alt-ergo.ocamlpro.com/tuto/tutorial.html) to introduce you to Alt-Ergo native syntax and program verification.
![](/blog/assets/img/screenshot_welcome_to_altergo_tutorial.png)
- A right panel composed of tabs:
- `Start` and `About` that contains general information about Alt-Ergo, Try-Alt-Ergo and how to use it.
- `Outputs` prints more information than the basic answer area under the editor. In these tabs you can find debugs (long) outputs, unsat-core or models (counter-example) generated by Alt-Ergo.
- `Options` contains every option you can use, such as the time limit / steps limit or to set the format of the input file to prove .
- `Statistics` is still a basic tab that only output axioms used to prove the input problem.
- `Examples` contains some basic examples showing the capabilities of our solver.
We hope you will enjoy this new version of Try-Alt-Ergo, we can't wait to read your feedback!
*This work was done at OCamlpro.*
......@@ -8,8 +8,6 @@ let old_to_new =
; ("/fr/recrutement-ocamlpro/", "/jobs")
; ( "https://www.ocamlpro.com/pre-inscription-a-une-session-de-formation-inter-entreprises/"
, "/" )
; ("https://www.ocamlpro.com/2021/01/22/release-of-alt-ergo-2-4-0/", "/")
; ("https://www.ocamlpro.com/2021/03/29/new-try-alt-ergo/", "/")
]
(* LEAD TO 404 *)
@ [ ("https://www.ocamlpro.com/2017/05/04/opam-build", "404")
......@@ -252,8 +250,11 @@ let old_to_new =
)
; ( "/2020/12/01/memthol-exploring-program-profiling/"
, "/blog/2020_12_01_memthol_exploring_program_profiling" )
; ( "/2021/01/22/release-of-alt-ergo-2-4-0/"
, "/blog/2021_01_22_release_of_alt_ergo_2_4_0" )
; ("/2021/02/02/2020-at-ocamlpro/", "/blog/2021_02_02_2020_at_ocamlpro")
; ("/2021/02/09/opam-2-0-8-release/", "/blog/2021_02_08_opam_2.0.8_release")
; ("/2021/03/29/new-try-alt-ergo/", "/blog/2021_03_29_new_try_alt_ergo")
; ( "/2021/04/29/alt-ergo-users-club-annual-meeting-2021/"
, "/blog/2021_04_29_reunion_annuelle_du_club_des_utilisateurs_dalt_ergo_2021"
)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment