-
Notifications
You must be signed in to change notification settings - Fork 323
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[scrape.yml] New OCaml Planet blog posts and videos (#2745)
Co-authored-by: cuihtlauac <[email protected]>
- Loading branch information
1 parent
8c0c109
commit f3af5ce
Showing
3 changed files
with
301 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| --- | ||
| title: MetAcsl v0.7 for Frama-C 29.0~ Copper | ||
| description: | ||
| url: https://frama-c.com/fc-plugins/metacsl.html | ||
| date: 2024-10-03T00:00:00-00:00 | ||
| preview_image: | ||
| authors: | ||
| - Frama-C | ||
| source: | ||
| --- | ||
|
|
||
|
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,246 @@ | ||
| --- | ||
| title: Alt-Ergo 2.6 is Out! | ||
| description: We are excited to announce the release of Alt-Ergo 2.6! Alt-Ergo is an | ||
| open-source automated prover used for formal verification in software development. | ||
| It is part of the arsenal behind static analysis frameworks such as TrustInSoft | ||
| Analyzer and Frama-C, and is one of the solvers behind Why3, a pla... | ||
| url: https://ocamlpro.com/blog/2024_09_01_alt_ergo_2_6_0_released | ||
| date: 2024-09-30T13:48:57-00:00 | ||
| preview_image: https://ocamlpro.com/blog/assets/img/alt-ergo-8-colors.png | ||
| authors: | ||
| - "\n Basile Cl\xE9ment\n " | ||
| source: | ||
| --- | ||
|
|
||
| <p></p> | ||
| <p> | ||
| </p><div class="figure"> | ||
| <p> | ||
| <a href="https://ocamlpro.com/blog/assets/img/alt-ergo-8-colors-blank-bg.png"> | ||
| <img src="https://ocamlpro.com/blog/assets/img/alt-ergo-8-colors-blank-bg.png" alt="The Alt-Ergo 2.6 release comes with many enhancements!"> | ||
| </a> | ||
| </p><div class="caption"> | ||
| The Alt-Ergo 2.6 release comes with many enhancements! | ||
| </div> | ||
| <p></p> | ||
| </div> | ||
| <p></p> | ||
| <p><strong>We are excited to announce the release of Alt-Ergo 2.6!</strong></p> | ||
| <p>Alt-Ergo is an open-source automated prover used for formal verification in | ||
| software development. It is part of the arsenal behind static analysis | ||
| frameworks such as TrustInSoft Analyzer and Frama-C, and is one of the | ||
| solvers behind Why3, a platform for deductive program verification. The newly | ||
| released version 2.6 brings new features and performance improvements.</p> | ||
| <p>Development on Alt-Ergo has accelerated significantly this past year, thanks to | ||
| the launch of the <a href="https://decysif.fr/en/">DéCySif</a> joint research project (i-Démo) | ||
| with AdaCore, Inria, OCamlPro and TrustInSoft. The improvements to bit-vectors | ||
| and algebraic data types in this release are sponsored by the Décysif project.</p> | ||
| <p>The highlights of Alt-Ergo 2.6 are:</p> | ||
| <ul> | ||
| <li>Support for reasoning and model generation with bit-vectors | ||
| </li> | ||
| <li>Model generation for algebraic data types | ||
| </li> | ||
| <li>Optimization with <code>(maximize)</code> and <code>(minimize)</code> | ||
| </li> | ||
| <li>FPA support is enabled by default and available in SMT-LIB format | ||
| </li> | ||
| <li>Binary releases now on GitHub | ||
| </li> | ||
| </ul> | ||
| <p>Alt-Ergo 2.6 also includes other improvements to the user interface (notably | ||
| the <code>set-option</code> SMT-LIB command), use of Dolmen as the default frontend for | ||
| SMT-LIB and native input, and many bug fixes.</p> | ||
| <h3>Bit-vectors</h3> | ||
| <p>In Alt-Ergo 2.5, we introduced built-in functions for the bit-vector | ||
| primitives from the SMT-LIB standard, but only provided limited reasoning | ||
| support. For Alt-Ergo 2.6, we set out to improve this reasoning support, and | ||
| have developed a new and improved relational theory for bit-vectors. This new | ||
| theory is based on an also new constraint propagation core that draws heavily | ||
| on the architecture of the Colibri solver (as in <a href="https://cea.hal.science/cea-01795779">Sharpening Constraint | ||
| Programming approaches for Bit-Vector Theory</a>), integrated into Alt-Ergo's | ||
| existing normalizing Shostak solver.</p> | ||
| <p>Bit-vectors are commonly used in verification of low-level code and in | ||
| cryptography, so improved support significantly enhances Alt-Ergo’s | ||
| applicability in these domains.</p> | ||
| <p>There are still areas of improvements, so please share any issue you encounter | ||
| with the bit-vector theory (or Alt-Ergo in general) via our | ||
| <a href="https://github.com/ocamlpro/alt-ergo/issues">issue tracker</a>.</p> | ||
| <p>To showcase improvements in Alt-Ergo 2.6, we compared it against the version | ||
| 2.5 and industry-leading solvers Z3 and CVC5 on a dataset of bit-vector | ||
| problems collected from our partners in the DéCySif project. The (no BV) | ||
| variants for Alt-Ergo do not use the new bit-vector theory but instead an | ||
| axiomatization of bit-vector primitives provided by Why3. The percentages | ||
| represent the proportion of bit-vector problems solved successfully in each | ||
| configuration.</p> | ||
| <table class="table"> | ||
| <thead> | ||
| <tr class="table-light text-center"> | ||
| <th scope="col"></th> | ||
| <th scope="col" colspan="2">AE 2.5</th> | ||
| <th scope="col" colspan="2">AE 2.6</th> | ||
| <th scope="col">Z3 (4.12.5)</th> | ||
| <th scope="col">CVC5 (1.1.2)</th> | ||
| <th scope="col">Total</th> | ||
| </tr> | ||
| <tr> | ||
| <th scope="row"></th> | ||
| <td>(BV)</td> | ||
| <td>(no BV)</td> | ||
| <td>(BV)</td> | ||
| <td>(no BV)</td> | ||
| <td></td> | ||
| <td></td> | ||
| <td></td> | ||
| </tr> | ||
| </thead> | ||
| <tbody> | ||
| <tr> | ||
| <th scope="row">#</th> | ||
| <td>4128</td> | ||
| <td>4870</td> | ||
| <td>6265</td> | ||
| <td>4940</td> | ||
| <td>5482</td> | ||
| <td>7415</td> | ||
| <td>9038</td> | ||
| </tr> | ||
| <tr> | ||
| <th scope="row">%</th> | ||
| <td>46%</td> | ||
| <td>54%</td> | ||
| <td>69%</td> | ||
| <td>54%</td> | ||
| <td>61%</td> | ||
| <td>82%</td> | ||
| <td>100%</td> | ||
| </tr> | ||
| </tbody> | ||
| </table> | ||
| <p>As the table shows, Alt-Ergo 2.6 significantly outperforms version 2.5, and the | ||
| new built-in bit-vector theory outperforms Why3's axiomatization. We even | ||
| surpass Z3 on this benchmark, a testament to the new bit-vector theory in | ||
| Alt-Ergo 2.6.</p> | ||
| <h3>Model Generation</h3> | ||
| <p>Bit-vector is not the only theory Alt-Ergo 2.6 improves upon. Model generation | ||
| was introduced in Alt-Ergo 2.5 with support for booleans, integers, reals, | ||
| arrays, enumerated types, and records. Alt-Ergo 2.6 extends this support to | ||
| bit-vector and arbitrary algebraic data types, which means that model | ||
| generation is now enabled for all the theories supported by Alt-Ergo.</p> | ||
| <p>Model generation allows users to extract concrete examples or counterexamples, | ||
| aiding in debugging and verification of their systems.</p> | ||
| <p>Model generation is also more robust in Alt-Ergo 2.6, with numerous bug fixes | ||
| and improvements for edge cases.</p> | ||
| <h3>Optimization</h3> | ||
| <p>Alt-Ergo 2.6 introduces optimization capabilities, available via SMT-LIB input | ||
| using OptiSMT primitives such as <code>(minimize)</code> and <code>(maximize)</code> and compatible | ||
| with Z3 and OptiMathSat. Optimization allows guiding the solver towards simpler | ||
| and smaller counterexamples, helping users find more concrete and realistic | ||
| scenarios to trigger a bug.</p> | ||
| <p>See some | ||
| <a href="https://ocamlpro.github.io/alt-ergo/latest/Optimization.html">examples</a> in the | ||
| documentation.</p> | ||
| <h3>SMT-LIB command support</h3> | ||
| <p>Alt-Ergo 2.6 supports more SMT-LIB syntax and commands, such as:</p> | ||
| <ul> | ||
| <li>The <code>(get-info :all-statistics)</code> command to obtain information about the | ||
| solver's statistics | ||
| </li> | ||
| <li>The <code>(reset)</code>, <code>(exit)</code> and <code>(echo)</code> commands | ||
| </li> | ||
| <li>The <code>(get-assignment)</code> command, as well as the <code>:named</code> attribute and | ||
| <code>:produce-assignments</code> option | ||
| </li> | ||
| </ul> | ||
| <p>See the <a href="https://smt-lib.org">SMT-LIB standard</a> for more details about these | ||
| commands.</p> | ||
| <h3>Floating-point theory</h3> | ||
| <p>In this release, we have made Alt-Ergo's <a href="https://ocamlpro.github.io/alt-ergo/next/Alt_ergo_native/05_theories.html#floating-point-arithmetic">floating-point | ||
| theory</a> | ||
| enabled by default: there is no need to provide the <code>--enable-theories fpa</code> | ||
| flag anymore. The theory can be disabled with <code>--disable-theories fpa,nra,ria</code> | ||
| (the <code>nra</code> and <code>ria</code> theories were automatically enabled along with the <code>fpa</code> | ||
| theory in Alt-Ergo 2.5).</p> | ||
| <p>We have also made the floating-point primitives available in the SMT-LIB | ||
| format as the indexed constant <code>ae.round</code> and the convenience <code>ae.float16</code>, | ||
| <code>ae.float32</code>, <code>ae.float64</code> and <code>ae.float128</code> functions; see the | ||
| <a href="https://ocamlpro.github.io/alt-ergo/v2.6.0/SMT-LIB_language/index.html#floating-point-arithmetic">documentation</a>.</p> | ||
| <h3>Dolmen is the new default frontend</h3> | ||
| <p>Introduced in Alt-Ergo 2.5, the Dolmen frontend has been rigorously tested for | ||
| regressions and is now the default for both <code>.smt2</code> and <code>.ae</code> files; the | ||
| <code>--frontend dolmen</code> flag that was introduced in Alt-Ergo 2.5 is no longer | ||
| necessary.</p> | ||
| <p>The Dolmen frontend is based on the <a href="https://github.com/gbury/dolmen">Dolmen</a> | ||
| library developed by Guillaume Bury at OCamlPro. It provides excellent support | ||
| for the SMT-LIB standard and is used to check validity of all new problems in | ||
| the SMT-LIB benchmark collection, as well as the results of the annual SMT-LIB | ||
| affiliated solver competition SMT-COMP.</p> | ||
| <p>The preferred input format for Alt-Ergo is now the SMT-LIB format. The legacy | ||
| <code>.ae</code> format is still supported, but is now deprecated and users are | ||
| encouraged to migrate to the SMT-LIB format if possible. Please <a href="mailto:[email protected]">reach | ||
| out</a> if you find any issue while migrating to | ||
| the SMT-LIB format.</p> | ||
| <p>As we announced when releasing Alt-Ergo 2.5, the legacy frontend (supports | ||
| <code>.ae</code> files only) is deprecated in Alt-Ergo 2.6, but it can still be | ||
| enabled with the <code>--frontend legacy</code> option. It will be removed entirely from | ||
| Alt-Ergo 2.7.</p> | ||
| <p>Parser extensions, such as the built-in AB-Why3 plugin, only work with the | ||
| legacy frontend, and will no longer work with Alt-Ergo 2.7. We are not | ||
| aware of any current users of either parser extensions or the AB-Why3 plugin: | ||
| if you need these features, please reach out to us on | ||
| <a href="https://github.com/ocamlpro/alt-ergo/issues">GitHub</a> or by | ||
| <a href="mailto:[email protected]">email</a> so that we can figure out a path | ||
| forward.</p> | ||
| <h3>Use of <code>dune-site</code> for plugins</h3> | ||
| <p>Starting with Alt-Ergo 2.6, we are using the plugin mechanism from | ||
| <code>dune-site</code> to replace the custom plugin loading <code>Dynlink</code>. Plugins now need | ||
| to be registered in the <code>(alt-ergo plugins)</code> site with the | ||
| <a href="https://dune.readthedocs.io/en/stable/reference/dune/plugin.html"><code>plugin</code> stanza</a>.</p> | ||
| <p>This does not impact users, but only impacts developers of Alt-Ergo plugins. See the | ||
| <a href="https://github.com/OCamlPro/alt-ergo/blob/next/src/plugins/fm-simplex/dune">dune file</a> | ||
| for Alt-Ergo's built-in FM-Simplex plugin for reference.</p> | ||
| <h3>Binary releases on GitHub</h3> | ||
| <p>Starting with Alt-Ergo 2.6, we will be providing binary releases on the | ||
| <a href="https://github.com/ocamlpro/alt-ergo/releases">GitHub Releases</a> page for | ||
| Linux (x86_64) and macOS (x86_64 and arm). These are released under the | ||
| same <a href="https://ocamlpro.github.io/alt-ergo/latest/About/licenses/index.html">licensing conditions</a> as the Alt-Ergo source code.</p> | ||
| <p>The binary releases are statically linked and have no dependencies, except | ||
| for system dependencies on macOS. They do not support dynamically loading | ||
| plugins.</p> | ||
| <h3>Performance</h3> | ||
| <p>For Alt-Ergo 2.6, our main focus of improvement in term of reasoning was on | ||
| bit-vectors and algebraic data types. Other theories also benefit from | ||
| broader performance improvements we made. On our internal | ||
| problem dataset, Alt-Ergo 2.6 is about 5% faster than Alt-Ergo 2.5 on the goals | ||
| they both prove.</p> | ||
| <h3>And more!</h3> | ||
| <p>This release also includes significant internal refactoring, notably | ||
| a rewrite from scratch of the interval domain. This improves the | ||
| accuracy of Alt-Ergo in handling interval arithmetic and facilitates mixed | ||
| operations involving integers and bit-vectors, resulting in shorter and more | ||
| reliable proofs.</p> | ||
| <p>See the complete changelog | ||
| <a href="https://ocamlpro.github.io/alt-ergo/v2.6.0/About/changes.html">here</a>.</p> | ||
| <p>We encourage you to try out Alt-Ergo 2.6 and share your experience or any | ||
| feedback on our <a href="https://github.com/OCamlPro/Alt-Ergo">GitHub</a> or by email at | ||
| <a href="mailto:[email protected]">[email protected]</a>. Your input will help | ||
| share future releases!</p> | ||
| <h3>Acknowledgements</h3> | ||
| <p>We thank the <a href="https://alt-ergo.ocamlpro.com/#club">Alt-Ergo Users' Club</a> members: AdaCore, the CEA, Thales, | ||
| Mitsubishi Electric R&D Center Europe (MERCE) and TrustInSoft.</p> | ||
| <p>Special thanks to David Mentré and Denis Cousineau at MERCE for funding the | ||
| initial optimization work. MERCE has been a Member of the Alt-Ergo Users' | ||
| Club for four years. This partnership allowed Alt-Ergo to evolve and we hope | ||
| that more users will join the Club on our journey to make Alt-Ergo a must-have | ||
| tool.</p> | ||
| <div class="figure"> | ||
| <div class="card-light blog-logos"> | ||
| <img src="https://ocamlpro.com/assets/img/logo_adacore.svg" alt="AdaCore logo"> | ||
| <img src="https://ocamlpro.com/blog/assets/img/cealist.png" alt="CEA list logo"> | ||
| <img src="https://ocamlpro.com/assets/img/logo_thales.svg" alt="Thales logo" style="height: 24px;"> | ||
| <img src="https://ocamlpro.com/assets/img/logo_merce.png" alt="Mitsubishi Electric logo"> | ||
| <img src="https://ocamlpro.com/assets/img/logo_trustinsoft.svg" alt="TrustInSoft logo" style="height: 32px;"> | ||
| </div> | ||
| <div class="caption">The dedicated members of our Alt-Ergo Club!</div> | ||
| </div> | ||
|
|
43 changes: 43 additions & 0 deletions
43
...rides/introducing-the-dune-developer-preview-a-new-era-for-ocaml-development.md
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,43 @@ | ||
| --- | ||
| title: 'Introducing the Dune Developer Preview: A New Era for OCaml Development' | ||
| description: The Dune team is excited to announce the arrival of Dune Developer Preview, | ||
| a major milestone for OCaml development! We've been working hard improving | ||
| url: https://tarides.com/blog/2024-10-03-introducing-the-dune-developer-preview-a-new-era-for-ocaml-development | ||
| date: 2024-10-03T00:00:00-00:00 | ||
| preview_image: https://tarides.com/blog/images/DDP-1360w~-GCJN60jJAv_blMzGyH5XQ.webp | ||
| authors: | ||
| - Tarides | ||
| source: | ||
| --- | ||
|
|
||
| <p>The Dune team is excited to announce the arrival of <a href="https://discuss.ocaml.org/t/ann-dune-developer-preview-updates/15160/7">Dune Developer Preview</a>, a major milestone for OCaml development! We've been working hard improving Dune, and we're excited to introduce this new way to ease OCaml workflows. If you are an OCaml developer, this is the time to explore the future of package management and development yourself.</p> | ||
| <h3>Why the Wait?</h3> | ||
| <p>Our progress has been slower than anticipated because the Dune project is a complex endeavour. We’re committed to balancing support for existing OCaml users while introducing new workflows. While opam remains the stable workflow and isn't going away, a key difference is that the Dune Developer Preview showcases experimental workflows. We believe, once fully ready, this will be transformative for the community. Meanwhile, we continue to maintain opam and its infrastructure, ensuring the OCaml ecosystem remains robust, with recent updates like opam 2.2 bringing proper Windows support.</p> | ||
| <h3>Why the Change?</h3> | ||
| <p>We have listened over time to your feedback and learned that while functional, the existing tooling around OCaml can be quite cumbersome. Our mission is to make OCaml development easier, faster and more enjoyable, and Dune is now about to become that all-in-one tool which does just that. This separation will allow Dune to cut down on the complexity and make its development process much lighter.</p> | ||
| <p>The Developer Preview gives a sneak peek into these improvements and provides an opportunity for developers to get their hands on these tools before the official release.</p> | ||
| <h3>What's New in Dune?</h3> | ||
| <p>The Dune Developer Preview introduces several major changes in how OCaml developers will work. Probably the most notable change is that it includes package management right within Dune itself. No more juggling with multiple tools; Dune does it all in one go.</p> | ||
| <p>Accordingly, the new Dune comes as a binary. That means it no longer requires the usage of opam to install it. You can simply just install Dune within minutes, and you'll be off to a flying start. That gives you so much more time for actual development.</p> | ||
| <h3>Drawing Inspiration from the Best</h3> | ||
| <p>Throughout this process, we've drawn inspiration from other successful ecosystems. We learned from Rust, Go, and Erlang the power of letting developers test and provide feedback on a pre-general release, and we are doing the same with Dune: giving the OCaml community a chance to have their say in shaping up the final form of this tool. Your input will be invaluable in refining Dune and ensuring it meets your needs.</p> | ||
| <h3>Join the Beta</h3> | ||
| <p>We are looking for developers to participate in the Dune Developer Preview. Experienced developers can help us put the latest features of Dune through their paces so that we can fine-tune the workflow to be smooth and intuitive across a range of projects. Those new to OCaml can test the workflow from their perspective of working in other ecosystems. Whether you have been using OCaml for years or are new to the OCaml ecosystem, your input is crucial in helping us make Dune the recommended tool for OCaml development.</p> | ||
| <p>To become a beta tester, one only needs to download the <a href="https://preview.dune.build/">Dune Developer Preview</a>. You will get the very latest version and immediately start playing with the new workflows and package management features. Your feedback will help to further shape the future of OCaml tooling, and we want to hear your thoughts on everything from usability to performance enhancements.</p> | ||
| <h3>Measuring Success</h3> | ||
| <p>Our goal is clear: use OCaml with as little ceremony as possible, so we set a few key benchmarks to make that happen. First: via Dune, the user should be able to fire up a new project in less than 10 seconds with no extra tooling required. This level of speed makes all the difference during everyday hacking.</p> | ||
| <p>We also monitor general developer satisfaction with the new Dune workflows. For the Net Promoter Score, we will know how likely a user is to recommend Dune to other users. Our objective is to reach +80, which shows great approval and satisfaction within the community.</p> | ||
| <h3>What's Next?</h3> | ||
| <p>This is only the beginning of the Dune Developer Preview. We will regularly update and enhance it based on feedback from beta testers. This includes polishing the new Dune Toolchain feature in order to automatically manage OCaml versions and development tools, and exploring new distribution channels in order for Dune to be even easier to download and use.</p> | ||
| <p>This is huge for OCaml, and we are excited to have you along for the ride. Why wait? Download the <a href="https://preview.dune.build/">Dune Developer Preview</a> today, and give some of the new workflows a try before letting us know what you think. With your help, we can make Dune the go-to tool for all OCaml development.</p> | ||
| <p>We can't wait to hear from you — and happy coding!</p> | ||
| <blockquote> | ||
| <p>At Tarides, our commitment to open source drives everything we do. We prioritise fostering the OCaml community and <a href="https://github.com/sponsors/tarides">advancing the development of the OCaml language</a>. We enjoy collaborating with industry partners and developers to continually enhance OCaml's performance and capabilities.</p> | ||
| </blockquote> | ||
| <blockquote> | ||
| <p>Tarides is also ready to explore commercial opportunities related to OCaml. Whether you need training, support, or custom development, we can help you adopt OCaml 5 more effectively. Please <a href="https://tarides.com/contact/">contact us</a> to discuss how we can assist you.</p> | ||
| </blockquote> | ||
| <blockquote> | ||
| <p>Become a part of the OCaml community, explore the language, and contribute to its growth.</p> | ||
| </blockquote> | ||
|
|