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

  • 723d72a7b5 Merge branch 'topic/kanig-win-patch' into 'master' master Johannes Kanig 2026-02-10 09:43:23 +00:00
  • a6dc469060 Check return codes of system calls Johannes Kanig 2026-02-10 10:13:41 +09:00
  • 128cbf77d7 Fix checking of error code of GetQueuedCompletionStatus Johannes Kanig 2026-02-10 10:02:43 +09:00
  • 572165c251 Cleanup of handled job object messages Johannes Kanig 2026-02-10 09:57:28 +09:00
  • c08c9144d9 Children of Windows server killed on exit Johannes Kanig 2026-02-10 09:18:57 +09:00
  • aa6a5b60ab Make Linux termination code safer Johannes Kanig 2026-02-10 09:18:28 +09:00
  • cf38d3ce38 Tentative fix for grandchildren Johannes Kanig 2026-02-05 18:55:45 +09:00
  • 60b0b618a6 Merge branch 'topic/fsf_merge_269/20251226' into 'fsf' fsf Marc Poulhiès 2026-01-13 08:55:26 +01:00
  • 50209174c0 Merge commit '9390baf120ef260547dfa14f08e11c890b203d9c' into topic/fsf_merge_269/20251226 Marc Poulhiès 2026-01-12 16:12:23 +01:00
  • 23421c3075 Merge branch 'topic/kanig-merge' into 'master' Johannes Kanig 2026-01-05 09:55:22 +00:00
  • 3262153853 Various postmerge adaptations Johannes Kanig 2025-12-15 17:51:17 +09:00
  • 244b0ee135 Regenerate configure Johannes Kanig 2025-12-15 17:51:02 +09:00
  • 68ed738789 Revert "[Debug_option] Use default ppxlib ast for better compatibility" Johannes Kanig 2025-12-15 17:14:38 +09:00
  • 25b13e2cab merge commit Johannes Kanig 2025-12-15 10:45:08 +09:00
  • e42c43804e Merge branch 'weekly_full_bench' into 'master' MARCHE Claude 2025-12-11 23:21:29 +01:00
  • efed8566d6 provers for reduced bench Claude Marche 2025-12-11 21:28:15 +01:00
  • 9fb8f8f2c7 bench reduced using bench image with more provers Claude Marche 2025-12-11 18:25:13 +01:00
  • 993ed183c1 Merge branch 'support-interfaces-in-parsing-api' into 'master' Benjamin Terra-Jorge 2025-12-11 16:53:06 +00:00
  • d33cd189df Update CHANGES.md and API doc Benjamin Jorge 2025-12-11 16:35:09 +01:00
  • d818a981f2 fix cmd line for E-prover 3.x Claude Marche 2025-12-11 16:29:16 +01:00
  • df84e66e41 bench run only manually Claude Marche 2025-12-11 14:29:35 +01:00
  • 1558726fcb proper renaming of E prover 2.6 Claude Marche 2025-12-11 13:24:15 +01:00
  • 3fe3c0b326 last attempt Claude Marche 2025-12-11 12:13:11 +01:00
  • 8e6377c940 again and againa and again Claude Marche 2025-12-11 12:10:40 +01:00
  • 4838becfba force remake image Claude Marche 2025-12-11 12:09:46 +01:00
  • 205cdd17fa remove again non working rule Claude Marche 2025-12-11 12:07:54 +01:00
  • 8acd97217c change image name, put back guard Claude Marche 2025-12-11 12:06:26 +01:00
  • 1082a636ec remove non working guard Claude Marche 2025-12-11 12:04:42 +01:00
  • 2095b61181 eprover and spass and Z3 4.14 Claude Marche 2025-12-11 12:03:25 +01:00
  • 9390baf120 Merge branch 'topic/kanig-272-imporve' into 'master' Johannes Kanig 2025-12-11 10:19:40 +00:00
  • 96debf4ef3 come on, let's fix again Claude Marche 2025-12-11 11:00:35 +01:00
  • c3c97aeb55 build image only for the branch commit, not the MR Claude Marche 2025-12-11 10:48:26 +01:00
  • bd88eb678a new image Claude Marche 2025-12-11 10:39:00 +01:00
  • 0f40e89fbc add E prover 2.6 Claude Marche 2025-12-11 10:29:15 +01:00
  • e19e373269 Merge branch 'topic/kanig-1110-merge' into '26.1' 26.2 26.1 Johannes Kanig 2025-12-10 23:48:02 +00:00
  • 8bb9da3b6b Merge branch '894-extraction-broken-when-cloning-a-module-with-interface' into 'master' Benjamin Terra-Jorge 2025-12-10 09:20:51 +00:00
  • 52776cb906 Merge branch 'improve-interface-api' into 'master' Benjamin Terra-Jorge 2025-12-10 09:17:32 +00:00
  • b7058e58c1 Merge branch '910-distinct-theories-with-the-same-ident' into 'master' Benjamin Terra-Jorge 2025-12-10 09:13:49 +00:00
  • 5be96e2b3c Merge branch 'improve_lse_hyps' into 'master' MARCHE Claude 2025-12-09 11:58:17 +01:00
  • 95c6f966ee adding package adduser Claude Marche 2025-12-09 11:16:32 +01:00
  • d879324ed5 upgrade DEbian version for bench Claude Marche 2025-12-09 11:10:41 +01:00
  • 05ec3c2e31 show ldd info for z3 Claude Marche 2025-07-10 10:11:38 +02:00
  • 3b71ffe67f z3 requires libstdc++ Claude Marche 2025-07-10 09:51:41 +02:00
  • b767de2cd1 cvc5 OK, z3 needs glibc Claude Marche 2025-07-09 17:01:43 +02:00
  • 1b7f37143e try with static versions of cvc5 Claude Marche 2025-07-09 16:47:17 +02:00
  • c75d4194c9 attempt to fix prover installation Claude Marche 2025-07-09 15:59:51 +02:00
  • 0c184d9297 upgrade policy for CVC5 Claude Marche 2025-07-09 13:38:47 +02:00
  • 9014bb8b92 update a session Claude Marche 2025-07-09 10:50:39 +02:00
  • ef62a72810 more upgraded sessions Claude Marche 2025-05-19 21:23:51 +02:00
  • 8cff58bc24 fix mistake Claude Marche 2025-05-19 21:03:05 +02:00
  • 7798158472 fix install of cvc5 1.1.x and 1.2.x Claude Marche 2025-05-19 20:54:02 +02:00
  • 7620017bbf upgraded provers in examples Claude Marche 2025-05-19 18:56:09 +02:00
  • 27884e1d27 more provers, replay restricted to real examples Claude Marche 2025-05-19 17:44:15 +02:00
  • 6126a56a0f add missing pkg zlib1g-dev Claude Marche 2025-05-15 09:16:55 +02:00
  • f61692625d add missing pkg-config Claude Marche 2025-05-14 11:36:49 +02:00
  • 8ef01fd1b3 Build another image with more versions of Alt-Ergo Claude Marche 2025-05-14 10:53:01 +02:00
  • c2c6798c6d use larger worker and longer timeout Claude Marche 2025-05-14 10:13:55 +02:00
  • ae4909d905 full bench Claude Marche 2025-04-30 10:49:51 +02:00
  • c75183288a New check kind for UC align Johannes Kanig 2025-12-01 11:49:44 +09:00
  • 01f80d6f50 relax hypothesis on a_max Claude Marche 2025-12-08 16:17:39 +01:00
  • 77afe4f97e Fix and improve prover failure reporting Johannes Kanig 2025-11-27 06:25:43 +00:00
  • 3c6bfd11e1 Merge branch 'topic/kanig-1110-ucalign' into 'master' Johannes Kanig 2025-12-05 09:38:54 +00:00
  • 4dc4c9117b Merge branch 'new-theory-seq-sum' into 'master' Jean-Christophe Filliâtre 2025-12-03 20:39:15 +01:00
  • 4bc892fd02 a better theory seq.Sum Jean-Christophe Filliatre 2025-12-03 19:01:11 +01:00
  • fdc76ccb86 Merge branch 'adjust_slse' into 'master' MARCHE Claude 2025-12-02 09:54:06 +01:00
  • 66a8b29530 improve proof of SLSE Claude Marche 2025-11-26 16:11:30 +01:00
  • d987c4b3b4 New check kind for UC align Johannes Kanig 2025-12-01 11:49:44 +09:00
  • 0d5e41a935 Merge branch 'hyp_name' into 'master' MARCHE Claude 2025-11-28 16:07:46 +01:00
  • 55247d3012 Merge branch 'information' into 'master' MARCHE Claude 2025-11-28 13:32:20 +01:00
  • c603015600 Don't generate hyp_name attribute if user already provided one Li-yao Xia 2025-11-28 13:07:48 +01:00
  • d43e0a0332 'informations' -> 'information' Li-yao Xia 2025-11-28 11:05:21 +01:00
  • c57969699b Merge branch 'topic/fsf_merge_269/20251119' into 'fsf' Marc Poulhiès 2025-11-28 00:59:29 +01:00
  • 758fc090dd Merge branch 'examples-avoid-iso-8859' into 'master' Guillaume Melquiond 2025-11-27 16:31:54 +01:00
  • 03ba36b21c Merge branch 'less-admits' into 'master' Guillaume Melquiond 2025-11-27 15:39:12 +01:00
  • df2cff5a59 Merge commit 'eea70d139ce2e4de5a1400d28b6c376ac1a895b8' into topic/fsf_merge_269/20251119 Marc Poulhiès 2025-11-27 14:02:21 +01:00
  • 9cb7ad7175 avoid iso-8859 encoding in examples Andre Maroneze 2025-11-27 09:46:37 +01:00
  • 4b24da8c83 Remove some admits in Coq realizations. Guillaume Melquiond 2025-11-27 09:42:21 +01:00
  • 3147d4a15f Merge branch 'fix-930' into 'master' Guillaume Melquiond 2025-11-26 16:59:48 +01:00
  • a4e12c4d54 Mark ppxlib < 0.33 as incompatible (fix #930). Guillaume Melquiond 2025-11-26 15:50:57 +01:00
  • 7fc0e55775 Merge branch 'topic/kanig-272-fail2' into 'master' Johannes Kanig 2025-11-26 00:05:08 +00:00
  • 1b24286b35 Merge branch 'generalize_lse' into 'master' MARCHE Claude 2025-11-25 12:34:29 +01:00
  • fc857b2fc2 proved udivexact generique Claude Marche 2025-11-25 11:26:25 +01:00
  • b9feb6aece proved mul generique Claude Marche 2025-11-24 17:30:25 +01:00
  • 06c14de8b0 fixed slse proof Claude Marche 2025-11-24 17:21:15 +01:00
  • 7a655e6952 fixed lemma gg_bounds Claude Marche 2025-11-24 12:47:35 +01:00
  • 4b373538ee Fix API examples Benjamin Jorge 2025-11-24 13:16:22 +01:00
  • d17a7b64b7 redone sum_accuracy and g_accuracy Claude Marche 2025-11-24 11:33:09 +01:00
  • 13410bfc8f cleaning Claude Marche 2025-11-24 11:22:11 +01:00
  • 9c60b5f0d6 add propagation in any format Claude Marche 2025-11-24 10:02:00 +01:00
  • 5870227f97 Merge branch 'pqueue-authors' into 'master' Jean-Christophe Filliâtre 2025-11-21 14:36:08 +01:00
  • f6f80d659d rendons à César... Jean-Christophe Filliatre 2025-11-21 13:26:28 +01:00
  • 9e63f81f86 Merge branch 'topic/fsf_merge_269/20251112' into 'fsf' Marc Poulhiès 2025-11-21 10:13:14 +01:00
  • 6f9b9a421a Merge commit 'c13da9842de1ab0c61c71d0320737a222ac366c2' into topic/fsf_merge_269/20251112 Marc Poulhiès 2025-11-21 10:10:43 +01:00
  • 350cc165aa Support module with interface in parsing API Benjamin Jorge 2025-11-06 18:38:10 +01:00
  • 7f385533d4 Share pmodule interface and implementation when possible Benjamin Jorge 2025-11-05 19:32:13 +01:00
  • 46c7861b2b Update CHANGES.md Benjamin Jorge 2025-05-05 16:22:44 +02:00
  • a07a1b6a88 Improve Pmodule API, update documentation Benjamin Jorge 2025-04-28 11:24:55 +02:00
  • 361c54b5c5 Fix trywhy3 Benjamin Jorge 2025-03-31 18:38:36 +02:00
  • 729a67f461 Store built-in modules with correct theories Benjamin Jorge 2025-03-26 14:57:45 +01:00
  • 25bf09e53a Reproduce #894 Benjamin Jorge 2025-01-15 14:35:16 +01:00