CI: fix the check for bad promoted files

This commit is contained in:
Louis Gesbert 2024-02-12 15:46:37 +01:00
parent c64503adf1
commit afcc435593
3 changed files with 14 additions and 10 deletions

View File

@ -88,7 +88,9 @@ jobs:
options: --user ocaml
steps:
- name: Check promoted files
run: cd /home/ocaml/catala && opam exec -- make check-promoted
run: |
cd /home/ocaml/catala && opam exec -- make check-promoted
git diff --exit-code
- name: Run tests
if: ${{ always() }}
run: cd /home/ocaml/catala && opam exec -- make tests

View File

@ -294,14 +294,15 @@ let transform_closures_scope_let ctx scope_body_expr =
{ ctx with name_context = Bindlib.name_of var_next })
scope_let.scope_let_expr
in
var_next,
Bindlib.box_apply (fun scope_let_expr ->
( var_next,
Bindlib.box_apply
(fun scope_let_expr ->
{
scope_let with
scope_let_expr;
scope_let_typ = Mark.copy scope_let.scope_let_typ TAny;
})
(Expr.Box.lift new_scope_let_expr))
(Expr.Box.lift new_scope_let_expr) ))
~last:(fun res ->
let _free_vars, new_scope_let_expr = (transform_closures_expr ctx) res in
(* INVARIANT here: the result expr of a scope is simply a struct

View File

@ -403,7 +403,8 @@ let generate_verification_conditions_code_items
(* We don't need to add the typ of the scope input var here
because it will never appear in an expression for which
we generate a verification conditions (the big struct is
destructured with a series of let bindings just after.) *);
destructured with a series of let bindings just
after.) *);
}
in
let _, vcs, asserts =