Denis Merigoux
a660987df0
Starting to implement closure conversion [skip ci]
2022-03-21 17:26:23 +01:00
Denis Merigoux
a7bdc0a114
Add condition for focusing the proof mode on a single scope
2022-03-17 17:44:24 +01:00
Denis Merigoux
bba5e3afea
Only print logging in Scopelang if debug
2022-03-16 12:00:36 +01:00
Denis Merigoux
c59451751b
Fix logging operator location for default justifications
2022-03-16 11:44:34 +01:00
Denis Merigoux
41cf1ec0e6
Merge pull request #222 from CatalaLang/refactor-catala_backend_option-functions
...
Refactor: group common functions related to backend_option in the Cli module
2022-03-09 11:12:01 +01:00
Louis Gesbert
b4b6d5d648
Fix compilation catala_web_interpreter
...
oops I overlooked that one
2022-03-08 17:35:57 +01:00
Louis Gesbert
729fb7e551
reformat (sync with master)
2022-03-08 16:12:25 +01:00
Louis Gesbert
071ec35234
Command-line: use a record for the options
...
Should make it much easier and less error-prone to add new options. There is
still a bit of boiler-plate, but at least it's contained in the Cli.options
function and doesn't transpire in the interfaces.
2022-03-08 16:11:39 +01:00
Emile Rolley
7c1f4cc02d
refactor: group common functions related to backend_option in the Cli module
2022-03-08 15:52:26 +01:00
Denis Merigoux
5bd66142a6
Big reformatting
...
ocamlformat 0.19.0 -> 0.20.1
100 -> 80 columns per line
Reestablished @emilerolley's smart fun break
2022-03-08 15:03:14 +01:00
Louis Gesbert
12ec65601d
Use format strings directly in debug/error/log functions
...
This avoids many intermediate calls to e.g. `Format.asprintf`; should result in
some cases in "more correct" use of `Format`¹, avoid the computation of unused
debug strings, and make the code more readable.
¹ for `Format` to work as expected, all intermediate calls need to go through
it. Some cases of formatting to an intermediate string then printing through Format
again are still present, but this makes the situation better.
2022-03-08 13:04:27 +01:00
Denis Merigoux
c65c38a2d5
Correct flag for enabling optimization
2022-02-24 16:46:02 +01:00
Denis Merigoux
756e7cb9b2
Merge branch 'master' into alain_default-option
2022-02-24 16:41:35 +01:00
Alain
73fe2f876c
Revert "Merge pull request #196 from CatalaLang/fixup-cmdliner"
...
fix cmdliner to 1.0.4
This reverts commit 8e1a1ccb634812830a25
2022-02-21 14:53:48 +01:00
Denis Merigoux
cab4e5c17e
Merge branch 'master' into alain_default-option
2022-02-15 10:20:53 +01:00
Denis Merigoux
1cec4b0721
Pretty-printer for scalc
2022-02-14 18:22:26 +01:00
Denis Merigoux
b25f64c3ae
Improve printing
2022-02-14 17:01:34 +01:00
Denis Merigoux
69a7465339
Merge branch 'master' into alain_default-option
2022-02-14 12:09:11 +01:00
Denis Merigoux
e1dc36f1b1
Merge branch 'master' into io-qualifiers-112-part-2
2022-02-10 22:59:37 +01:00
Denis Merigoux
b6d9d7cf5f
Update Cmdliner with breaking changes
2022-02-10 22:57:07 +01:00
Denis Merigoux
30061b8c86
Better encoding of inputs [skip ci]
2022-02-09 11:37:52 +01:00
Denis Merigoux
97f8875a39
Merge branch 'master' into alain_default-option
2022-02-04 15:35:52 +01:00
Denis Merigoux
6cf1b768d2
Fix bug in Python backend producing unreachable code
2022-02-01 15:41:53 +01:00
Denis Merigoux
edeba14692
Just typechecking for compiler
2022-01-31 15:28:19 +01:00
Denis Merigoux
5e253ba321
Disabling exact counterexamples values from CI testing because of randomness
2022-01-26 16:24:09 +01:00
Denis Merigoux
b11e3329b3
Functorize VC solving IO [skip ci]
2022-01-18 18:51:02 +01:00
Denis Merigoux
d705334d9e
Merge branch 'master' into proof_platform
2022-01-11 15:43:33 +01:00
Denis Merigoux
2b6e7c8b98
Working prototype of clerk, the new build system for Catala
2022-01-10 17:57:58 +01:00
Aymeric Fromherz
a9ebfaed38
Pass program to z3encoder
2022-01-10 14:36:15 +01:00
Denis Merigoux
4082e5056e
More prettier things
2022-01-10 10:59:30 +01:00
Denis Merigoux
3a864b6160
Aesthetic improvements
2022-01-10 10:28:14 +01:00
Denis Merigoux
743a1b74c9
Renamed and grouped modules cleanly
2022-01-08 18:37:04 +01:00
Denis Merigoux
546107bfb0
Merge branch 'proof_platform' of github.com:CatalaLang/catala into proof_platform
2022-01-07 18:37:30 +01:00
Denis Merigoux
50224851f5
Port optimizations to Dcalc
2022-01-07 18:36:56 +01:00
Aymeric Fromherz
1105858bea
Setting up the pipeline for encoding VCs to Z3
2022-01-07 17:50:45 +01:00
Denis Merigoux
75ef1ef70f
Added proof of concept of verification condition generation
2022-01-07 12:04:31 +01:00
Emile Rolley
397b0e1d7c
fix(build/doc): remove warnings due to .ml* files
2022-01-02 14:53:51 +01:00
Alain
16b0dba9d0
Merge branch 'master' into feat/default-option
2021-12-14 10:27:11 +01:00
Denis Merigoux
9f0929b86d
Fix the final bug!
2021-12-10 17:55:24 +01:00
Denis Merigoux
f16ebf8b8b
Removed optimizations, just one weird bug missing [skip ci]
2021-12-10 17:23:14 +01:00
Denis Merigoux
00a998462a
Implementation OK, now on to debugging Bindlib [skip ci]
2021-12-10 16:30:36 +01:00
Denis Merigoux
50400c445d
Few progress
2021-12-09 23:29:49 +01:00
Denis Merigoux
c456a62cb3
Builds but with empty stubs [skip ci]
2021-12-09 22:59:39 +01:00
Denis Merigoux
7d3e381d45
Improvements with Alain during weekly meeting
2021-11-24 15:51:49 +01:00
Alain
f75341c44f
making options default compilation target
2021-11-22 15:55:21 +01:00
Denis Merigoux
b56299f3d3
Switch ocamlformat to 0.19.0
2021-08-19 11:35:56 +02:00
Denis Merigoux
817b1785df
Python translation working but still buggy
2021-06-24 17:50:08 +02:00
Denis Merigoux
eb9c75f394
Making progress into translation
2021-06-23 17:47:34 +02:00
Denis Merigoux
1313183353
Defining a new intermediate representation
2021-06-22 16:01:57 +02:00
Denis Merigoux
fffd0ffb63
Working the way into the Python backend
2021-06-22 14:55:43 +02:00
