ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

Commit Graph

  • c717b82bc7 More careful check of record type Matteo Manighetti 2025-02-14 16:13:09 +01:00
  • 0547089061 Fix floats in check_ce Matteo Manighetti 2025-02-14 15:55:20 +01:00
  • ac0414db88 Fix bv_length in concrete floats Matteo Manighetti 2025-02-14 15:04:55 +01:00
  • 6655fe3c8e Some work on floats Matteo Manighetti 2025-02-14 14:46:34 +01:00
  • e1667ac285 Update oracles Matteo Manighetti 2025-02-14 08:53:42 +01:00
  • 54820773e8 Convert concrete epsilon terms in check_ce and not in model_parser Matteo Manighetti 2025-02-14 08:53:14 +01:00
  • 8a1fed69f9 Fix space leak: replace global Hid with Wid Li-yao Xia 2025-02-05 14:43:50 +01:00
  • 7420460454 Merge branch 'simplify-rac-api' into 'master' MARCHE Claude 2025-02-10 18:20:22 +01:00
  • 7b3ec0ad7d Check_ce: simplify API interface Matteo Manighetti 2025-02-10 18:20:22 +01:00
  • ee8f8711cb Merge branch 'minimum-excludant-other-versions' into 'master' Jean-Christophe Filliâtre 2025-02-02 09:25:46 +01:00
  • 500312de2a minimum excludant example Jean-Christophe Filliatre 2025-02-01 21:22:20 +01:00
  • 67f040aba3 Handle exception when file is not found Li-yao Xia 2024-12-23 11:57:10 +01:00
  • 6e52fc95c9 Merge branch 'upgrade-altergo-2.6.0' into 'master' MARCHE Claude 2025-01-17 14:31:49 +01:00
  • ee522d818d SMTv2 model parser: don't fail on untyped prover variables Matteo Manighetti 2024-12-16 09:59:54 +01:00
  • 2841eb1da6 Prevent stackify from breaking hypothesis_selection. Guillaume Melquiond 2025-01-17 08:01:32 +01:00
  • d0dd9b4ccb Fix incorrect invokation of the OCaml compiler. Guillaume Melquiond 2025-01-17 07:59:52 +01:00
  • 108850e55d Mark stackify as incompatible with OCaml < 4.12. Guillaume Melquiond 2025-01-16 16:00:48 +01:00
  • 8266a266de Merge branch 'topic/kanig-489-tree' into 'master' Johannes Kanig 2025-01-15 09:03:21 +00:00
  • 7a46b14d36 Adapt Why3 tree to gnat2why changes Johannes Kanig 2025-01-09 11:20:41 +09:00
  • 6bbb0a06ef Helper script to upgrade provers and detect regressions Matteo Manighetti 2025-01-14 19:44:24 +01:00
  • cbbc713860 Allow why3session to select timeout nodes Matteo Manighetti 2025-01-14 17:07:00 +01:00
  • 7ae65be566 Upgrade sessions to use Alt-Ergo 2.6.0 Matteo Manighetti 2024-12-12 15:06:46 +01:00
  • 70ed0a8608 Merge branch 'topic/779-dross-exit_cases' into 'master' Claire Dross 2024-12-18 09:26:44 +00:00
  • 1a92d492e2 Add attributions to changelog. Guillaume Melquiond 2024-12-11 11:24:39 +01:00
  • 3f66c6e298 Use more links to the standard library in the documentation. Guillaume Melquiond 2024-12-11 11:04:49 +01:00
  • 59fde1a829 Fix some documentation typos. Guillaume Melquiond 2024-12-11 11:04:18 +01:00
  • 793182e71e Disable warnings coming from model parser Matteo Manighetti 2024-12-16 15:06:56 +01:00
  • df1fd4541e Merge branch 'smtv2-dont-fail-on-untyped-prover-vars' into 'master' MARCHE Claude 2024-12-16 09:59:55 +01:00
  • 23c0f93c02 SMTv2 model parser: don't fail on untyped prover variables Matteo Manighetti 2024-12-16 09:59:54 +01:00
  • c04b008016 Merge remote-tracking branch 'why3-inria/master' into why3-devel Matteo Manighetti 2024-12-13 17:34:11 +01:00
  • efeac5d981 Bump version. Guillaume Melquiond 2024-12-12 10:56:56 +01:00
  • 88f8a1408c Update Opam files. Guillaume Melquiond 2024-12-12 09:40:32 +01:00
  • 187fd52100 Version 1.8.0 Guillaume Melquiond 2024-12-11 14:20:34 +01:00
  • 9e231d5119 Merge branch 'mailmap' into 'master' Guillaume Melquiond 2024-12-11 12:31:19 +01:00
  • 7b8a8ccba3 Merge branch 'windows-support' into 'master' Guillaume Melquiond 2024-12-11 11:19:28 +01:00
  • 5905590630 Add windows compilation support Basile Desloges 2024-12-11 11:19:28 +01:00
  • 45d834f9cd add ref to doc in CHANGES Claude Marche 2024-12-11 10:36:55 +01:00
  • 2d846b7d1f Remove unused variable. Guillaume Melquiond 2024-12-07 09:18:12 +01:00
  • 0269e91228 Update documentation a bit. Guillaume Melquiond 2024-12-07 09:14:16 +01:00
  • 0b4e9e74bc Mark OCaml 4.09 as the minimal supported version as it is the only one tested. Guillaume Melquiond 2024-12-07 09:14:01 +01:00
  • 82c4513767 Update and clean changelog. Guillaume Melquiond 2024-12-06 20:33:36 +01:00
  • 15a06a679a apidoc: Fix formatting of link Li-yao Xia 2024-12-02 14:07:14 +01:00
  • 137c1472a4 Remove some trailing spaces. Guillaume Melquiond 2024-11-29 08:26:10 +01:00
  • 8a86d9ac62 Update copyright years. Guillaume Melquiond 2024-11-29 08:15:19 +01:00
  • 479fc1a339 Remove unused proofs. Guillaume Melquiond 2024-11-29 08:05:01 +01:00
  • ba63400497 Update mailmap. Guillaume Melquiond 2024-11-29 07:55:30 +01:00
  • 4b29289b61 Update mailmap. Paul Patault 2024-09-12 23:45:43 +02:00
  • 84c22882f3 Merge branch 'build-image' into 'master' Guillaume Melquiond 2024-12-07 09:00:45 +01:00
  • dddedb6e15 Clean js_of_ocaml rules a bit. Guillaume Melquiond 2024-12-07 05:27:03 +01:00
  • 798649f938 Update the OCaml compilers, avoid installing Alt-Ergo twice, and run the build-image job less often. Guillaume Melquiond 2024-12-06 17:37:30 +01:00
  • 144516556b Merge branch 'bugfix/v1.7' Guillaume Melquiond 2024-12-06 20:38:57 +01:00
  • f2f5c5357c Merge branch '887-upgrade-alt-ergo-version-for-ce-checking-to-2-6-0' into 'master' MARCHE Claude 2024-12-06 16:09:37 +01:00
  • 8d9026f3ac Move CE oracles to Alt-Ergo 2.6.0 Matteo Manighetti 2024-12-06 16:09:37 +01:00
  • 9f7f6e8d13 Add VC kind for exit cases and change id of VC kinds for cases Claire Dross 2024-12-06 13:16:56 +01:00
  • 02c65ddab7 Merge branch 'smtv2-unparsed-sexp' into 'master' MARCHE Claude 2024-11-29 23:07:38 +01:00
  • 13bde17dae Warn about errors in model parsing for counterexamples Matteo Manighetti 2024-11-29 23:07:38 +01:00
  • 1f692dbb55 Merge branch 'coma_record_split' into 'master' Andrei Paskevich 2024-11-28 19:06:25 +01:00
  • 5b9a766db5 coma: avoid splitting records when factorizing Andrei Paskevich 2024-11-28 16:42:30 +01:00
  • d41309a7d3 coma: minor Andrei Paskevich 2024-11-28 14:31:21 +01:00
  • ff34f32622 Merge branch 'coma_record_split' into 'master' Andrei Paskevich 2024-11-28 14:05:22 +01:00
  • 128528db40 coma: ignore implicit imports for record splitting Andrei Paskevich 2024-11-28 11:38:33 +01:00
  • f6c30906c2 Merge branch 'fix-889' into 'master' Guillaume Melquiond 2024-11-27 20:24:08 +01:00
  • 349162ea1a Scroll to a location before applying colors in the IDE (fix #889). Guillaume Melquiond 2024-11-27 18:04:09 +01:00
  • 4189321ea6 Merge branch 'coma_record_split' into 'master' Andrei Paskevich 2024-11-27 16:16:56 +01:00
  • b282db6b67 Merge branch 'improved-declarations-doc' into 'master' Guillaume Melquiond 2024-11-27 15:38:03 +01:00
  • 93d4646a98 improved documentation Jean-Christophe Filliâtre 2024-11-27 15:38:02 +01:00
  • 379d56b1d7 coma: simplify record manipulations on the fly Andrei Paskevich 2024-11-26 02:17:52 +01:00
  • 4363d3ad4f Merge branch 'fix_session_sudoku' into 'master' MARCHE Claude 2024-11-27 12:02:29 +01:00
  • 4c5c4ce6b7 fix session sudoku Claude Marche 2024-11-27 09:50:11 +01:00
  • a6f7544382 Merge branch 'fix_another_sessions' into 'master' MARCHE Claude 2024-11-18 18:31:08 +01:00
  • 9a20078a8e fix sessions Claude Marche 2024-11-18 15:54:18 +01:00
  • ec97d9abc0 Merge branch 'fix_sessions' into 'master' MARCHE Claude 2024-11-16 11:40:18 +01:00
  • 5f9169e032 fis sessions Claude Marche 2024-11-16 09:41:34 +01:00
  • 746f2fa7c1 Merge branch 'more_numeric' into 'master' MARCHE Claude 2024-11-15 19:45:56 +01:00
  • 01ea2c9f1b Merge branch 'fix_proof_coincidence_count' into 'master' MARCHE Claude 2024-11-15 17:55:03 +01:00
  • ae24b5d7fd added LSE examples with fixed values for size Claude Marche 2024-11-15 16:18:25 +01:00
  • 6b31aa87ba ease the proof of coincidence count Claude Marche 2024-11-15 15:39:22 +01:00
  • f448f491ad Merge branch 'extensional' into 'master' MARCHE Claude 2024-11-14 20:03:57 +01:00
  • 2e1d53f51b fix sessions and CE oracles Claude Marche 2024-11-14 14:48:30 +01:00
  • cabea44347 fix realizations Claude Marche 2024-11-12 13:35:44 +01:00
  • 37bd944fa5 two forms of transformation extensionality Claude Marche 2024-11-12 10:41:07 +01:00
  • 0e86c23d93 add regression test from BTS Claude Marche 2024-11-08 15:02:58 +01:00
  • 904a1b6e9e Update bench. Guillaume Melquiond 2024-10-30 17:56:21 +01:00
  • 94a1bb848f Factor out the sequence "inline_trivial" to "remove_unused", and add "extensionality" to it. Guillaume Melquiond 2024-10-30 17:32:20 +01:00
  • 46d53c02a9 Mark some types as having an extensional equality. Guillaume Melquiond 2024-10-30 17:24:06 +01:00
  • 27e140d729 Add a transformation "extensionality" to help with proofs of equality. Guillaume Melquiond 2024-10-28 17:30:49 +01:00
  • 2610486871 Merge branch 'zarith' into 'master' Guillaume Melquiond 2024-11-09 09:19:48 +01:00
  • 38b25abe53 Miscellaneous fixes. Guillaume Melquiond 2024-11-08 16:38:42 +01:00
  • 35601b77e7 Switch to zarith (fix #298). Guillaume Melquiond 2024-11-08 16:30:15 +01:00
  • dd1930d7b1 Reverse the logic for building the Docker image. Guillaume Melquiond 2024-11-08 16:34:37 +01:00
  • 9f427cff28 Merge branch 'coq-string' into 'master' Guillaume Melquiond 2024-11-08 16:05:00 +01:00
  • a7d0370df3 Add missing Coq definition for BuiltIn.string. Guillaume Melquiond 2024-11-08 13:48:11 +01:00
  • 72777db628 Merge branch 'fmap_additional_operators' into 'master' MARCHE Claude 2024-11-08 12:08:37 +01:00
  • c000797178 Additional operators for fmaps Claude Marche 2024-11-08 10:15:33 +01:00
  • 1af03cedb2 Merge branch 'cherry-pick-2ab57e21' into '25.1' 25.2 25.1 25-sustained Joffrey Huguet 2024-11-06 09:21:02 +00:00
  • e8c7fac406 Merge branch 'topic/71-kanig-colibri' into 'master' Joffrey Huguet 2024-11-05 10:54:02 +00:00
  • 086280c982 Merge branch 'fix-example-rightmost-bit-trick' into 'master' MARCHE Claude 2024-11-04 15:51:07 +01:00
  • 435cd76b65 remove use of cvc5 1.2.0 Claude Marche 2024-11-04 13:49:14 +01:00
  • 697236590f Merge branch 'improved-proof-of-rightmostbittrick' into 'master' MARCHE Claude 2024-11-03 21:25:05 +01:00
  • 38e88735a6 Merge branch '585-new-function-for-conversion-from-real-to-float' into 'master' MARCHE Claude 2024-11-03 21:13:11 +01:00