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

  • 3fafd800f5 Fix wrongly named field in doc Johannes Kanig 2025-08-28 16:14:33 +09:00
  • 5c280f548c Merge branch 'coma-tests' into 'master' PATAULT Paul 2025-08-27 12:57:40 +02:00
  • 6e847f2de7 coma: apply updated syntax in tests Paul Patault 2025-08-27 11:40:41 +02:00
  • 55e45070d2 Merge branch 'topic/kanig-424-line' into 'master' Johannes Kanig 2025-07-28 09:14:09 +00:00
  • a5be2ff017 Minor cleanup Johannes Kanig 2025-07-28 17:49:40 +09:00
  • 344d3f3145 Merge branch 'topic/kanig-424-line' into 'master' Johannes Kanig 2025-07-28 08:48:33 +00:00
  • 174cca9a41 Parse limit-line spec with multiple file:line items Johannes Kanig 2025-07-25 16:55:09 +09:00
  • f0b5206c94 Merge branch 'coma_smarter_scc' into 'master' Andrei Paskevich 2025-07-25 21:02:27 +02:00
  • a5898d4657 coma_logic: ignore fake dependencies in mutually recursive handlers Andrei Paskevich 2025-07-24 20:00:25 +02:00
  • c6a2003402 Merge branch 'sqrt2_irrational_simplified' into 'master' Jean-Christophe Filliâtre 2025-07-17 13:21:43 +02:00
  • 77224d610a sqrt 2 irrational simplified Jean-Christophe Filliatre 2025-07-17 10:45:45 +02:00
  • 878b048a55 Merge branch 'sqrt2_irrational' into 'master' Jean-Christophe Filliâtre 2025-07-15 11:33:59 +02:00
  • d897058b4e new example: sqrt 2 is irrational Jean-Christophe Filliatre 2025-07-15 10:16:12 +02:00
  • 846d822aee Merge branch 'structural_variants' into 'master' Andrei Paskevich 2025-07-09 10:21:55 +02:00
  • 88514de302 vc: extend default wf-ordering for algebraic variants Andrei Paskevich 2025-07-08 16:03:15 +02:00
  • 4c9bc01d25 Merge branch 'insertion_sort_list' into 'master' Andrei Paskevich 2025-06-30 15:40:02 +02:00
  • b2d3a442c2 examples/insertion_sort_list: add a couple of variants Andrei Paskevich 2025-06-30 14:31:45 +02:00
  • e9d2a4476c Merge branch 'insertion-sort-list' into 'master' Jean-Christophe Filliâtre 2025-06-27 10:12:25 +02:00
  • f74b24dba0 new example: insertion sort on lists, variant Jean-Christophe Filliatre 2025-06-26 17:30:36 +02:00
  • a53ba8ed97 Merge branch 'compat-5.4-using-ppxlib' into 'master' François Bobot 2025-06-19 10:20:54 +02:00
  • e00dca0a34 update release instructions after release Claude Marche 2025-06-06 10:21:52 +02:00
  • c8eb5fe35a Merge branch 'topic/kanig-954-altergo' into 'master' Johannes Kanig 2025-06-18 07:49:48 +00:00
  • 2ffed5e451 Adopt upstream changes for alt-ergo driver Johannes Kanig 2025-06-18 10:57:20 +09:00
  • c0d28bd80c Alt-Ergo 2.6 driver, functions on reals, float rounding Johannes Kanig 2025-06-06 12:00:50 +02:00
  • 89a894b47a do not map IEEE floats theory to Alt-Ergo's own theory MARCHE Claude 2025-05-22 19:49:00 +02:00
  • f959ccab08 Merge branch 'ressurect_sudoko_js' into 'master' MARCHE Claude 2025-06-17 20:18:42 +02:00
  • 666a0a402f Merge branch 'js-nat-to-zarith' into 'master' MARCHE Claude 2025-06-17 19:59:07 +02:00
  • e6c94d3a1d make sudoku web page work again Claude Marche 2025-03-25 16:14:09 +01:00
  • 9b5393e6f1 Compile again programs extracted to OCaml and JS Claude Marche 2025-04-02 14:37:47 +02:00
  • 5c26a709ba Merge branch '891-why3-pp-add-support-for-val-declarations' into 'master' MARCHE Claude 2025-06-17 18:10:39 +02:00
  • 39bd8c20e0 pp of let/val program function (spec only) MARCHE Claude 2025-06-17 18:10:39 +02:00
  • 63aa797499 Merge branch '917-improve-why3-pp' into 'master' MARCHE Claude 2025-06-13 20:00:46 +02:00
  • 08563517d7 minor improvements in Why3 pp latex output Claude Marche 2025-06-13 18:59:40 +02:00
  • a5a3b326b5 Merge branch 'fix_alter_ergo_driver_no_ae_sqrt_real' into 'master' MARCHE Claude 2025-06-13 09:24:48 +02:00
  • 116c0aa789 There is no symbol ae.sqrt_real parsed by Alt-Ergo 2.6 Claude Marche 2025-06-11 10:08:46 +02:00
  • 1e14d162fc Merge branch 'avoid_assert_failure_on_session_merging' into 'master' MARCHE Claude 2025-06-12 19:52:03 +02:00
  • 30b439d8b5 fix issue with file Ids in sessions Claude Marche 2025-06-11 10:08:46 +02:00
  • a4483b13c0 Merge branch 'produce_special_float_values_in_model' into 'master' MARCHE Claude 2025-06-11 13:09:37 +02:00
  • ff86d53bf2 Produce special float values in counterexamples MARCHE Claude 2025-06-11 13:09:37 +02:00
  • 3b07721f87 [Debug_option] Use default ppxlib ast for better compatibility François Bobot 2025-06-11 09:28:16 +02:00
  • 21e6fc95fb Adapt ppx_debug_optim to ppxlib Benjamin Jorge 2025-06-06 16:45:29 +02:00
  • af87976e65 Merge branch 'topic/kanig-905-altergo' into 'master' MARCHE Claude 2025-06-06 12:00:50 +02:00
  • 0082a6412a Alt-Ergo 2.6 driver, functions on reals, float rounding Johannes Kanig 2025-06-06 12:00:50 +02:00
  • b723bd4add update release doc Claude Marche 2025-06-04 11:15:46 +02:00
  • 50f084bf55 Merge branch 'bugfix/v1.8' Claude Marche 2025-06-04 11:10:16 +02:00
  • b9fe989f75 Version 1.8.1 Claude Marche 2025-06-04 10:59:28 +02:00
  • e991d73789 update headers Claude Marche 2025-06-04 10:51:30 +02:00
  • 4a95bf2863 prepare release Claude Marche 2025-06-04 10:49:46 +02:00
  • 695db5347e Merge branch 'topic/kanig-6-sig' into 'fsf-15' fsf-15 Johannes Kanig 2025-06-04 08:05:38 +00:00
  • 119b36cc71 Improve compatibility with C23 (fix #901). Guillaume Melquiond 2025-02-20 17:35:20 +01:00
  • 8ee7946672 Merge branch 'topic/891-proof-potentially-invalid' into 'master' Claire Dross 2025-05-27 12:20:31 +00:00
  • 09e34a9c0b Merge branch '905-alt-ergo-driver-creates-inconsistencies-for-floating-points' into 'master' MARCHE Claude 2025-05-22 19:49:00 +02:00
  • d547f17f49 do not map IEEE floats theory to Alt-Ergo's own theory MARCHE Claude 2025-05-22 19:49:00 +02:00
  • 036e25d7b9 Merge branch '898-ide-file-path-attributes-on-modules-containing-are-not-normalized' into 'master' MARCHE Claude 2025-05-22 19:48:01 +02:00
  • 78c9852cab ensures paths are normalized for theories and files Claude Marche 2025-05-22 14:02:01 +02:00
  • 0912c7b3cc New check kind for validity checks Claire Dross 2025-05-05 15:54:22 +02:00
  • d16e72f322 Merge branch 'improved-binomial-coefficient' into 'master' Jean-Christophe Filliâtre 2025-05-20 16:37:40 +02:00
  • cdd0075d0e binomial coefficient example: alternative loop Jean-Christophe Filliatre 2025-05-20 14:35:38 +02:00
  • 7de53213bd Merge branch 'topic/kanig-854-fsf' into 'master' Johannes Kanig 2025-05-20 09:26:53 +00:00
  • bc2749b358 Use correct runners for github builds Johannes Kanig 2025-05-07 10:10:19 +09:00
  • ed5ffafd36 Merge branch 'topic/kanig-854-fsf' into 'fsf-15' Johannes Kanig 2025-05-15 09:10:06 +00:00
  • abd01c9ede Add Linux arm builds for FSF 15 Johannes Kanig 2025-05-15 09:27:14 +09:00
  • 442fa7966b Merge branch 'list-distinct-recursive-not-inductive' into 'master' Jean-Christophe Filliâtre 2025-05-14 17:32:28 +02:00
  • 53b3249062 list.Distinct using a recursive definition Jean-Christophe Filliâtre 2025-05-14 17:32:28 +02:00
  • 1307365f43 Merge branch 'topic/kanig-854-fsf' into 'fsf-15' fsf-15.1.0 Johannes Kanig 2025-05-13 09:08:21 +00:00
  • 9cd080a32f doc: exclude '_' from lident_nq Li-yao Xia 2025-05-13 10:48:09 +02:00
  • f16e3281eb Use correct runners for MacOS ARM/x86-64 Johannes Kanig 2025-05-13 16:49:31 +09:00
  • cb403741c4 Merge branch 'topic/kanig-918-ci' into 'master' Johannes Kanig 2025-05-09 07:32:57 +00:00
  • 27d5be983e Windows and Linux builds for Why3 CI Johannes Kanig 2025-05-08 17:36:16 +09:00
  • 2db4a5dd76 Merge branch 'map-permut-permutation' into 'master' Jean-Christophe Filliâtre 2025-05-08 14:31:25 +02:00
  • bf65ee24f0 Merge branch 'topic/kanig-854-workflow' into 'master' Johannes Kanig 2025-05-08 08:15:43 +00:00
  • 8544f5aab3 Allow manual running of github workflow Johannes Kanig 2025-05-08 16:49:35 +09:00
  • 665573c0ab Fix github workflow Johannes Kanig 2025-04-18 18:54:32 +09:00
  • e9dda0e0ad stooge_sort: simplified proof Jean-Christophe Filliatre 2025-05-08 08:27:19 +02:00
  • 1ef45fa90c Merge branch 'topic/kanig-854-alt-ergo' into 'fsf-15' Johannes Kanig 2025-05-08 01:23:20 +00:00
  • c928811d2d map.MapPermut is a permutation Jean-Christophe Filliatre 2025-05-07 23:43:38 +02:00
  • 30e22ee03b enable MacOS intel builds Johannes Kanig 2025-05-07 10:10:19 +09:00
  • c04edb90d7 New driver for alt-ergo 2.6 SMT input Johannes Kanig 2025-05-07 09:58:53 +09:00
  • abad541687 Add windows compilation support Basile Desloges 2024-12-11 11:19:28 +01:00
  • 58dce00be2 Fix github workflow Johannes Kanig 2025-04-18 18:54:32 +09:00
  • ff5849b000 Merge branch 'slowsort' into 'master' Jean-Christophe Filliâtre 2025-05-06 20:10:13 +02:00
  • 4bca1a2984 Merge branch 'stooge-sort' into 'master' Jean-Christophe Filliâtre 2025-05-06 19:47:35 +02:00
  • 70d4e57dfe new example: slowsort Jean-Christophe Filliatre 2025-05-06 18:20:12 +02:00
  • 84232fb688 new example: Stooge sort Jean-Christophe Filliatre 2025-05-06 18:04:16 +02:00
  • 6db1a4816f Merge branch 'bugfix/v1.8' Guillaume Melquiond 2025-05-02 15:51:23 +02:00
  • aa3493525e Merge branch 'java-bench' into 'master' Guillaume Melquiond 2025-04-30 14:13:39 +02:00
  • 751ff8f3f7 Avoid mistakenly run the java bench if there is a runtime but no compiler. Guillaume Melquiond 2025-04-30 10:41:34 +02:00
  • 30ad1d9b0c Merge branch 'doc-nq' into 'master' Guillaume Melquiond 2025-04-25 18:04:38 +02:00
  • 6fff6b57c3 Fix clone injectivity Benjamin Jorge 2025-03-13 15:54:10 +01:00
  • c243ef1062 Handle exception when file is not found Li-yao Xia 2024-12-23 11:57:10 +01:00
  • 41487cc80b Change detection order to favor recent versions of Vampire. Guillaume Melquiond 2025-04-02 10:57:01 +02:00
  • ff4999aba1 Remove default limits on interactive provers. Guillaume Melquiond 2025-04-25 11:34:59 +02:00
  • 4dd2deeaa4 Fix space leak: replace global Hid with Wid Li-yao Xia 2025-02-05 14:43:50 +01:00
  • 9dd2cca4a9 Merge branch 'interactive-limits' into 'master' Guillaume Melquiond 2025-04-25 17:17:36 +02:00
  • b911211124 Remove default limits on interactive provers. Guillaume Melquiond 2025-04-25 11:34:59 +02:00
  • 0687abff5e doc: Fix production rules for suffix, lident_nq, uident_nq, qident to agree with lexer.mll Li-yao Xia 2025-04-09 15:46:38 +02:00
  • 506936145d Merge branch 'topic/kanig-why3-config' into 'master' Johannes Kanig 2025-04-08 23:36:57 +00:00
  • 128fda7873 Zarith is now mandatory, no need to mention in config output Johannes Kanig 2025-04-08 18:31:28 +09:00
  • 025cb451bc Merge branch 'topic/kanig-794-configure' into 'master' Johannes Kanig 2025-04-07 23:47:44 +00:00
  • 30467a4ddd Update configure after why3 merge Johannes Kanig 2025-04-07 09:58:10 +00:00