AFAIK, opam doesn't impose any licensing restrictions to add/publish a
new package :-)
Regards,
- Mohamed.
On 23/03/2020 18:21, François Bobot wrote:
Le 19/03/2020 à 17:14, Albin Coquereau a écrit :
Note that Alt-Ergo of course remains available for academic or exploratory
purpose under
dIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Hello,
Yes ! we are working on this. It's a matter of days (or hours).
- Mohamed.
On 13/02/2019 08:55, Ralf Treinen wrote:
Hello,
On Tue, Feb 12, 2019 at 09:09:06PM -0700, Jerry James wrote:
On Tue, Feb 12, 2019 at 3:21 AM Mohamed Iguernlala wrote:
As usual, you can report bugs, ask
, Feb 12, 2019 at 11:21 AM Mohamed Iguernlala
mailto:iguer.a...@gmail.com>> wrote:
Release of Alt-Ergo 2.3.0
Dear Alt-Ergo users,
We are happy to announce the release of Alt-Ergo 2.3.0. You can
get the sources from the website: https://alt-ergo.ocamlpro.com.
OPAM pa
for this week. Don't
hesitate to contact us if you want to join the Club and to support
Alt-Ergo development.
As usual, you can report bugs, ask questions, or give your
feedback regarding this version, or Alt-Ergo in general:
https://github.com/OCamlPro/alt-ergo/issues
Best regards,
Mohamed Iguernlala
On 24/01/2019 14:37, Julia Lawall wrote:
Are there some particular arguments that why3 provides to alt-ergo? Now I
am just running a proof in altgr-ergo, and it has been running for more
than 5 minutes with no result - it looks like an infinite loop. But from
within why3, the lemma is accepted
On 24/01/2019 13:50, Julia Lawall wrote:
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote:
Hello,
You can use "alt-ergo -profiling N " to display some
profiling information on standard output every "N"
seconds (you'll probably need a big screen or to put a smaller
font siz
Hello,
You can use "alt-ergo -profiling N " to display some
profiling information on standard output every "N"
seconds (you'll probably need a big screen or to put a smaller
font size for the terminal's text). There are 5 different views,
and you are probably interested in the last one. To cycle
your feedback.
Best regards,
Mohamed Iguernlala.
[1] https://github.com/OCamlPro/alt-ergo/blob/2.1.0/sources/CHANGES
---
Senior R Engineer @ OCamlPro
Research Associate, VALS team, LRI
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979
Hi,
I just tried to understand what's happening with this example:
- I noticed that only CVC4 1.4 proves the example with "get
counter-example" option. Version 1.5 does not.
- I used the bisect capability of Why3 to generate a smaller VC
that is proved with CVC4-1.4 + "get
7 at 01:57:09PM +0100, Mohamed Iguernlala wrote:
>
> > More generally, in addition to license update,
>
> The change of license is also quite important - the new license allows
> only for non-commercial use. This means that debian will not be able to
> include any version of AltErgo
This is related to strategies as explained in page 63 of the manual:
http://why3.lri.fr/download/manual-0.88.0.pdf
Regards,
- Mohamed.
On 13/10/2017 19:22, Gerlach, Jens wrote:
With a clean install of opam I had no problems to install why3-0.88.0.
By the way, when calling ‘why3 config
Hello,
OPAM repository's continuous integration tools are becoming
really strict and check a lot of situations and cases before a
new package is accepted.
Why3 0.88.0 has been proposed 7 days ago, but it's still not
included in the repo:
https://github.com/ocaml/opam-repository/pull/10413
--
Mohamed Iguernlala
Senior R Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.xyz
LinkedIn: https://fr.linkedin.com/in/mohamed-iguernlala-71515979
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https
Treinen a écrit :
Hi Mohamed,
On Mon, Nov 21, 2016 at 12:55:18PM +0100, Mohamed Iguernlala wrote:
A new version of Alt-Ergo (v. 1.30) is released. The tarball, a
Windows binary, and a Javascript version are available on Alt-Ergo's
website at:
https://alt-ergo.ocamlpro.com/
configure gives me
fixes (see
CHANGES [1]). But, the main new feature is experimental support for
models generation. More details about this extension are available
here [2].
Please, don't hesitate to report bugs, to ask questions, or to give
your feedback.
Best regards,
Mohamed Iguernlala.
[1] https://github.com
16 matches
Mail list logo
