Denis Merigoux
365037f70c
Correctly bench
2022-09-26 13:28:07 +02:00
Denis Merigoux
463b0965e3
Same example in Puython and in JS
2022-09-26 13:28:07 +02:00
Denis Merigoux
3f62a99b7a
Remove erroneous import
2022-09-26 13:28:07 +02:00
Denis Merigoux
32c89cc3a2
Fix Python backend for housing benefits
2022-09-26 13:28:07 +02:00
Denis Merigoux
89b625642f
Money from int and not from float
2022-09-26 13:28:06 +02:00
Denis Merigoux
431a0b99c1
Initial writeup of Python calling to housing benefits
2022-09-26 13:28:06 +02:00
Catala nix updated
e53f6b6087
update lock files
2022-09-26 00:28:43 +00:00
Louis Gesbert
84c1063509
Change the clerk tests to use inline output ( #340 )
2022-09-23 17:06:05 +02:00
Louis Gesbert
8c1696d0ff
Inline tests: cleanup trailing whitespace
2022-09-23 16:56:21 +02:00
Louis Gesbert
fe6fabb1b0
Clerk tests: update README
2022-09-23 16:41:22 +02:00
Louis Gesbert
005de24ee7
Inline tests: ensure proper escaping of output
...
and that the input is not truncated with --reset
2022-09-23 14:52:04 +02:00
Louis Gesbert
0c0ef1ae1a
Add test return codes
...
Simply re-generated with 'make tests CLERK_OPTS=--reset'
2022-09-23 14:50:02 +02:00
Louis Gesbert
0ab7a0f9ce
Turn all existing tests to inline tests
...
Done using
```bash
process() { FILE=$1; awk 'match($0, /^```catala-test *{ *id *= *"(.*)" *}/, a) {print "```catala-test-inline"; f="'"$(dirname $FILE)/output/$(basename $FILE)"'." a[1]; getline; print "$ " $0; while ((getline<f) > 0) print; next} {print}' $FILE >$FILE.new; mv $FILE.new $FILE; }
for f in tests/test_*/*/*.catala_* examples/**/*.catala_*; do process $f; git add $f; done
for d in $(find -name output -type d); do git rm -r $d; done
```
2022-09-23 14:45:10 +02:00
Louis Gesbert
b9c0453fc9
Clerk tests: add ability to have tests with inlined output
...
Reduces the number of files, and makes tracking and diffing tests much easier.
2022-09-23 13:50:56 +02:00
Denis Merigoux
19beb91262
gnu gedit syntax highlighting ( #336 )
2022-09-20 14:37:12 +02:00
Denis Merigoux
754174390b
Merge branch 'master' into yueli_master
2022-09-20 12:01:11 +02:00
Louis Gesbert
58f7e6bab8
Clerk: don't default to infinite ninja jobs ( #337 )
2022-09-20 11:51:37 +02:00
Louis Gesbert
6cb8ee7916
Clerk: don't default to infinite ninja jobs
2022-09-20 11:30:29 +02:00
Denis Merigoux
c7f07435fc
Moved doc around
2022-09-20 10:50:43 +02:00
Denis Merigoux
cc8c460fb3
Remove chinese language support as it is not yet supported by the compiler
2022-09-20 10:44:46 +02:00
YueLiPicasso
9c3b001f21
gnu gedit syntax highlighting
2022-09-20 16:15:46 +08:00
Denis Merigoux
f1d0831d86
LégiFrance<->Catala connector ( #329 )
2022-09-19 11:14:21 +02:00
Catala nix updated
fbd6b07372
update lock files
2022-09-19 00:26:12 +00:00
Louis Gesbert
1b97f55c00
Add a few tests on typing errors
...
the `err6` test also highlights that Typecheck errors get overly delayed
2022-09-15 17:28:05 +02:00
Aymeric Fromherz
e7c3ef604e
Do not hardfail when pretty-printing unknown Z3 variables ( #333 )
...
This PR extends PR #331 , by avoiding hard failures when pretty-printing
a Z3 model when generating a counterexample.
#331 added some Z3 variables to encode EMatch nodes that are only used
internally in the encoding, and do not correspond to any source
variable. When trying to retrieve the source variable corresponding to
this Z3 variable for pretty-printing purposes (stored in a map in the
context, called ctx.z3_vars), we thus had a hard OCaml failure due to a
Not_found exception.
This PR fixes this by ignoring internal variables during pretty-printing
of the counterexample. It also adds some unit tests for #331 , although,
since counterexample generation is disabled in tests/, this specific
issue would not have been caught.
Fixes #332
2022-09-13 20:20:56 +02:00
Aymeric Fromherz
2c5b3dd25e
Add unit tests for extension of Z3 backend to non-bool EMatch nodes
2022-09-13 16:05:33 +02:00
Aymeric Fromherz
7f07274c1f
Ignore unfound (i.e., internal) variables during Z3 model printing
2022-09-13 15:54:26 +02:00
Denis Merigoux
99627ff3dc
Better Z3 encoding of EMatch nodes ( #331 )
...
Now that #272 was merged and that type information is available at every
AST node, this PR improves the Z3 encoding of pattern matching in the
verification backend. To do so, it implements the second solution
presented in #241 .
Fixes #241
2022-09-13 11:49:55 +02:00
Aymeric Fromherz
fee64d6f6f
format
2022-09-13 10:37:30 +02:00
Aymeric Fromherz
b7854eb6f3
Z3Backend: Use type information inside AST node for match translation
2022-09-13 10:33:02 +02:00
Aymeric Fromherz
ea13981c5d
Match annotation type in io.mli and in Z3 backend
2022-09-12 18:10:02 +02:00
Aymeric Fromherz
0592cdab2a
Z3encoding: Use auxiliary variable for encoding type-generic EMatch
2022-09-12 17:52:55 +02:00
Catala nix updated
f6840f45b3
update lock files
2022-09-12 00:25:43 +00:00
Denis Merigoux
6e64f769a0
Update assets and rename executable
2022-09-08 15:16:39 +02:00
Denis Merigoux
a4207c9d9e
Last corrections
2022-09-08 14:54:02 +02:00
Denis Merigoux
1df20c18ac
Fixing discrepancies with LegiFrance in French housing benefits
2022-09-08 12:30:16 +02:00
Denis Merigoux
3188ac5e13
Starting to fix diffs
2022-09-07 17:51:48 +02:00
Denis Merigoux
dba9b40ff6
Restore diff checking
2022-09-07 17:51:41 +02:00
Denis Merigoux
3accabe03a
Update assets
2022-09-07 17:26:40 +02:00
Denis Merigoux
3756a6fb22
Fix french housing benefits
2022-09-07 17:14:36 +02:00
Denis Merigoux
8445174a5b
Improvements to expiration checking
2022-09-07 17:14:22 +02:00
Denis Merigoux
0670dd697f
Correct expiration checking
2022-09-07 13:03:12 +02:00
Denis Merigoux
09fc71c625
Differenciating API requests depending on text ID (beginning)
2022-09-06 18:32:26 +02:00
Denis Merigoux
19ba5ce923
Don't process everything at the same time
2022-09-06 18:00:22 +02:00
Denis Merigoux
1990b0b970
Code compiles
2022-09-06 17:25:57 +02:00
Denis Merigoux
2ffafdbd3a
Bring back files from ancient git history
2022-09-06 15:56:36 +02:00
Denis Merigoux
166f0a732d
Opam update for static binaries
2022-09-06 14:42:45 +02:00
Denis Merigoux
0e3616d8ef
Update assets
2022-09-06 14:27:56 +02:00
Denis Merigoux
d7e219b0dd
Correct test output for proof mode
2022-09-06 14:10:32 +02:00
Denis Merigoux
84b994b521
Bug caught with proof mode
2022-09-05 17:35:44 +02:00
