Commit Graph

Select branches

Hide Pull Requests

17

18-sustained

18.0

18.1

18.2

19-sustained

19.0

19.1

19.2

20-sustained

20.0

20.1

20.2

21-sustained

21.0

21.1

21.2

22-sustained

22.0

22.1

22.2

23-sustained

23.0

23.1

23.2

24-sustained

24.0

24.1

24.2

25-sustained

25.0

25.1

25.2

26.0

26.1

26.2

a2c2-2020

fsf

fsf-11.2

fsf-12

fsf-13

fsf-14

fsf-15

gpl-2013

gpl-2014

gpl-2015

gpl-2016

gpl-2017

gpl-2018

lri-colibri

lri-float_test

lri-itp

lri-master

lri-spark-float-smtlib

lts-18

lts-19

lts-20

lts-21

master

newsystem

oxford_cde

spark-14.0

spark-15.0

spark-16.0

why3_polymorphism_smt

#3

fsf-15.1.0

Mono Color

• d5181abb09 Merge branch '876-ide-crashes-when-clicking-on-goal' into 'master' MARCHE Claude 2024-09-26 18:10:56 +02:00
• dc10b72ac7 do not fail when goal as no loc when stack_trace is enabled Claude Marche 2024-09-26 16:00:53 +02:00
• 1aff0e0deb Merge branch 'coma_fixes' into 'master' Andrei Paskevich 2024-09-26 13:38:24 +02:00
• 1e5c04769f coma: eval_match expects all the implicit module imports Andrei Paskevich 2024-09-26 11:34:34 +02:00
• 4bda4fe757 Merge branch 'example-r-cos-theta' into 'master' MARCHE Claude 2024-09-26 09:24:48 +02:00
• 3bb628674d new example for numeric strategy Claude Marche 2024-09-24 15:14:35 +02:00
• 045c9fd0f6 Merge branch 'coma_fixes' into 'master' Andrei Paskevich 2024-09-23 11:17:10 +02:00
• 9c2a1d926f Merge branch 'rac-incomplete-better-trace' into 'master' MARCHE Claude 2024-09-20 08:41:30 +02:00
• 6d3be09d94 RAC: Add new exception for cases where context is available Matteo Manighetti 2024-09-20 08:41:30 +02:00
• f3a2f7cc34 coma: add Fany Andrei Paskevich 2024-09-19 13:31:08 +02:00
• 79192cae28 coma: apply eval_match to VCs and inferred pre-/post-conditions Andrei Paskevich 2024-09-19 13:28:03 +02:00
• 55ace476d9 Merge branch '306-add-program-equality-on-boolean-type' into 'master' MARCHE Claude 2024-09-19 10:54:25 +02:00
• 7dd2b50449 Pmodule: t->t->t functions can be overloaded as X->X->t functions MARCHE Claude 2024-09-19 10:54:24 +02:00
• cb9a1a02ee Merge branch '638-fix-usage-of-optional-argument-me_name_trans-in-functions-on-models' into 'master' MARCHE Claude 2024-09-19 10:46:18 +02:00
• 853d09433d get rid of print_model_human and the filter_similar param of print_model MARCHE Claude 2024-09-19 10:46:18 +02:00
• 69ee4236f4 Merge branch 'fix_missing_edited_files' into 'master' MARCHE Claude 2024-09-18 18:21:15 +02:00
• 55e3d335ca fix session having extra edited files Claude Marche 2024-09-18 15:42:05 +02:00
• 4d0131dc3e Merge branch '848-get-rid-of-option-json-values-in-why3prove' into 'master' MARCHE Claude 2024-09-18 15:24:34 +02:00
• 7f1c78a541 Simplify option for printing JSON counterexamples Matteo Manighetti 2024-09-17 13:27:33 +02:00
• 10660a621b Merge branch 'coma_fixes' into 'master' Andrei Paskevich 2024-09-18 10:30:02 +02:00
• b6f9d81e2e coma: replace levels with a neutrality status + protected handler set Andrei Paskevich 2024-09-17 19:14:12 +02:00
• fd81557dc8 Merge branch 'coma_fixes' into 'master' Andrei Paskevich 2024-09-17 14:41:43 +02:00
• 62d0917edb Merge branch 'bvconverter256' into 'master' MARCHE Claude 2024-09-17 13:14:05 +02:00
• 9137a0403e Define converters from various BV sizes to 256 bits Jacques-Henri Jourdan 2024-09-17 13:14:05 +02:00
• a5024a38ce coma: fix wrong levels in factorize and missing negations in t_neg Andrei Paskevich 2024-09-17 12:20:23 +02:00
• ccb4a6ee72 Merge branch '855-driver-alt-ergo-fpa-should-not-use-the-ae-builtin-for-abs-on-reals' into 'master' MARCHE Claude 2024-09-17 10:44:53 +02:00
• 6e3d21b5f0 check that real.FromInt.from_int is correctly sent to Alt-Ergo MARCHE Claude 2024-09-17 10:44:53 +02:00
• 13d15d836f Merge branch '870-call_provers-analyze_result-defaults-to-unknown' into 'master' MARCHE Claude 2024-09-16 17:16:19 +02:00
• 7d1bf6a2cc suggestion for better handling of unrecognized answers Matteo Manighetti 2024-09-16 17:16:17 +02:00
• 42a4bcf87f Merge branch 'document-extraction-to-C' into 'master' MARCHE Claude 2024-09-13 14:35:51 +02:00
• c9c58c695f Augment documentation of extraction to C Claude Marche 2024-09-13 11:05:21 +02:00
• 2e496ee045 Merge branch 'verifythis_2024_solutions' into 'master' PATAULT Paul 2024-09-12 17:34:52 +02:00
• 602f1007ba new examples: verifythis 2024 solutions to challenges 0 and 1 Jean-Christophe Filliatre 2024-09-12 15:28:53 +02:00
• ecd825d49d Merge branch 'knuth-bubble-sort' into 'master' Jean-Christophe Filliâtre 2024-09-05 21:11:55 +02:00
• 114fc686a9 new example: Knuth's bubble sort Jean-Christophe Filliatre 2024-09-05 19:11:32 +02:00
• 9371ad18ab Merge branch 'coma-only' into 'master' PATAULT Paul 2024-09-04 10:19:12 +02:00
• e6adb1e601 added constraint for js_of_ocaml version (5.6.0 minimum) Paul Patault 2024-09-03 18:48:46 +02:00
• 0cbe48541f Merge branch 'list-length-via-peano' into 'master' MARCHE Claude 2024-09-03 11:09:31 +02:00
• 59cb8a7de0 List length via peano MARCHE Claude 2024-09-03 11:09:30 +02:00
• 6c21707f07 Merge branch 'list-length-as-int63' into 'master' MARCHE Claude 2024-09-02 13:55:43 +02:00
• 792edc39d7 Merge branch 'proofs-without-fpa' into 'master' MARCHE Claude 2024-09-02 13:21:56 +02:00
• 4791086e9e compute a list length as a 63-bit integer Claude Marche 2024-09-02 11:27:27 +02:00
• 052edfd29e no need for FPa for these proofs Claude Marche 2024-09-02 11:13:06 +02:00
• 9e0bec8310 rename gnat_objectives to gnat_checks Johannes Kanig 2024-09-02 09:25:26 +09:00
• 2478f2ce88 rename objective to check Johannes Kanig 2024-09-02 09:13:20 +09:00
• ff2e8223fc rename reason to check_kind Johannes Kanig 2024-09-02 08:18:43 +09:00
• 045f120ce1 Merge branch 'topic/593-kanig-json' into 'master' 25.0 Johannes Kanig 2024-08-13 23:51:37 +00:00
• 0d93cf5c2f Refactoring of JSON printing Johannes Kanig 2024-08-14 08:38:01 +09:00
• a2a17213cd Merge branch 'topic/593-kanig-jsonmin' into 'master' Johannes Kanig 2024-08-13 23:20:00 +00:00
• 5f244a2459 Print JSON on single line, no spaces Johannes Kanig 2024-08-13 16:12:37 +09:00
• 40a7b4fc93 coma: added documentation section Paul Patault 2024-08-08 11:43:40 +02:00
• e0f5cd626b coma: update changes.md Paul Patault 2024-08-08 09:34:49 +02:00
• bb708cfec0 coma: added examples Paul Patault 2024-07-25 11:46:18 +02:00
• 000fd2d347 coma: update stdlib + examples Paul Patault 2024-07-05 12:15:40 +02:00
• bf775596c8 coma: generalize let%attr in let%span Paul Patault 2024-06-04 18:07:26 +02:00
• 9ef8eabe50 coma: examples of the paper Paul Patault 2024-05-15 19:22:54 +02:00
• 171104e310 coma: expl attributes Paul Patault 2024-04-16 18:25:55 +02:00
• ddb799e96d coma: add attributes to pre/post if given in type decl Paul Patault 2024-04-10 18:03:59 +02:00
• 2289c712c2 coma: fix lexer mli warning Paul Patault 2024-04-10 18:03:42 +02:00
• 23f1a47aae coma: proto let%attr let%file Paul Patault 2024-04-08 16:14:26 +02:00
• b956a79701 coma: weird handlers (wip) Andrei Paskevich 2024-04-04 14:33:08 +02:00
• b8d7dabd30 coma: update examples/coma/asm.coma Andrei Paskevich 2024-03-30 15:18:04 +01:00
• a948e516bd coma_logic: fix missing effects in mutully recursive definitions Andrei Paskevich 2024-03-30 15:17:27 +01:00
• df73ef05dc coma: one barrier per cycle Andrei Paskevich 2024-03-30 11:45:55 +01:00
• 06c41d6495 coma: minor Andrei Paskevich 2024-03-29 22:59:48 +01:00
• 626ba943e7 coma: assembly code example Jean-Christophe Filliatre 2024-03-29 11:16:19 +01:00
• b220a78935 coma: do not precompute unneeded subVCs Andrei Paskevich 2024-03-27 23:19:45 +01:00
• a0929f218d coma_typing: specced outcomes cannot appear before type or data parameters Andrei Paskevich 2024-03-14 00:42:41 +01:00
• cc48752b42 coma: accept Church's dot in handler applications Andrei Paskevich 2024-03-14 00:06:32 +01:00
• 323313623d coma_logic: simplify 'C x y = C u v' into 'x = u /\ y = v' Andrei Paskevich 2024-03-13 23:38:08 +01:00
• 4ab78a9f61 coma: eliminate trivial equalities more aggressively Andrei Paskevich 2024-03-10 23:39:52 +01:00
• c015ebabbe coma: debug flag "coma_no_trivial" discards trivial VC goals Andrei Paskevich 2024-03-10 22:24:45 +01:00
• 29804b3ddd coma: make "rec" optional in top-level definitions Andrei Paskevich 2024-03-10 22:13:47 +01:00
• 25de89f4cc coma: tests with polymorphism Paul Patault 2024-03-01 20:45:07 +01:00
• f4ca2cc68b coma_logic: cosmetic Andrei Paskevich 2024-03-01 21:27:22 +01:00
• a5cbb9b2fd coma_logic: test & fix Andrei Paskevich 2024-03-01 18:07:41 +01:00
• cfa3c44778 coma: effect inference Andrei Paskevich 2024-03-01 17:47:27 +01:00
• 6be7f4230d coma: minor Andrei Paskevich 2024-02-29 23:23:31 +01:00
• 6f0198513a coma_logic: tweaks and fixes Andrei Paskevich 2024-02-29 22:57:26 +01:00
• 47da32fdc5 coma: effect inference (wip) Andrei Paskevich 2024-02-28 15:48:03 +01:00
• 56d73fbc85 examples/re.coma: better spec Andrei Paskevich 2024-02-27 17:30:23 +01:00
• 90ca25b8d7 coma: accept meta declarations Andrei Paskevich 2024-02-26 23:43:44 +01:00
• 95adb14325 coma: accept WhyML keywords as Coma lidents Andrei Paskevich 2024-02-26 19:23:38 +01:00
• ec40aa57b7 coma: WIP RE Paul Patault 2024-02-26 18:50:18 +01:00
• d6807794a6 coma: restrict the place of preconditions and let-bindings in prototypes Andrei Paskevich 2024-02-26 15:52:55 +01:00
• c2bd152551 coma: modules export handlers Andrei Paskevich 2024-02-26 13:49:40 +01:00
• 9c97b66f70 coma_main: piggyback on top of WhyML modules, not theories Andrei Paskevich 2024-02-26 11:03:14 +01:00
• 043139f78d coma: minor Andrei Paskevich 2024-02-26 00:41:57 +01:00
• 4c7d019b1b coma: drop symbol counting in coma_typing (moved to coma_logic) Andrei Paskevich 2024-02-26 00:07:41 +01:00
• b76edd3ca1 coma: support --debug parse_only Andrei Paskevich 2024-02-25 17:51:22 +01:00
• c06ff36f93 coma: remove unneeded barriers from re.coma Andrei Paskevich 2024-02-25 17:27:18 +01:00
• 4b07f12456 coma: minor Andrei Paskevich 2024-02-25 17:18:22 +01:00
• 446c75ce2a coma: moved RE.coma to use new syntax Paul Patault 2024-02-25 17:18:36 +01:00
• 86694e5b4b coma: do not put the terms in curly braces in let- and set- blocks Andrei Paskevich 2024-02-25 16:24:07 +01:00
• af9b24a5bd coma: remove the commented noise from re.coma Andrei Paskevich 2024-02-25 16:13:07 +01:00
• bf3d7858cd coma: new prototype syntax (with let-definitions and annotations) Andrei Paskevich 2024-02-25 15:47:37 +01:00
• 95580e5dbc coma: RE done Paul Patault 2024-02-25 14:09:26 +01:00
• 6ea6ae87f9 coma_logic: tweaks and fixes Andrei Paskevich 2024-02-25 11:03:11 +01:00
• 4ec58e243b coma: accept "ASSUME { formula } expr" Andrei Paskevich 2024-02-25 01:43:36 +01:00
• d4f3d02e7f coma_logic: recognize definitions that do not produce VCs Andrei Paskevich 2024-02-25 01:12:24 +01:00