Commit 675a6edf authored by Dario Pinto's avatar Dario Pinto
Browse files

add art, upd url

parent 24ff235f
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!
......@@ -8,7 +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 *)
......@@ -252,6 +251,8 @@ 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/04/29/alt-ergo-users-club-annual-meeting-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