Restore JS executable of the Catala compiler

[denismerigoux]

The problem

Right now, if you compile the Catala interpreter with js_of_ocaml to a Javascript binary with

dune build compiler/catala.bc.js --profile release

You will get the following errors:

Dummy implementations (raising 'Failure' exception) will be used if they are not available at runtime.
You can prevent the generation of dummy implementations with the commandline option '--disable genprim'
Missing primitives:
  caml_mutex_new
  caml_thread_initialize
  n_add_rec_def
  n_ast_map_contains
  n_ast_map_erase
  n_ast_map_find
  n_ast_map_insert
  n_ast_map_keys
  n_ast_map_reset
  n_ast_map_size
  n_ast_map_to_string
  n_ast_to_string
  n_ast_vector_get
  n_ast_vector_push
  n_ast_vector_resize
  n_ast_vector_set
  n_ast_vector_size
  n_ast_vector_to_string
  n_ast_vector_translate
  n_context_of_ast
  n_context_of_ast_map
  n_context_of_ast_vector
  n_context_of_func_entry
  n_context_of_func_interp
  n_context_of_model
  n_context_of_param_descrs
  n_context_of_params
  n_context_of_solver
  n_context_of_symbol
  n_del_config
  n_func_decl_to_string
  n_func_entry_get_arg
  n_func_entry_get_num_args
  n_func_entry_get_value
  n_func_interp_get_else
  n_func_interp_get_entry
  n_func_interp_get_num_entries
  n_get_app_arg
  n_get_app_decl
  n_get_app_num_args
  n_get_arity
  n_get_as_array_func_decl
  n_get_ast_hash
  n_get_ast_id
  n_get_ast_kind
  n_get_datatype_sort_constructor
  n_get_datatype_sort_constructor_accessor
  n_get_datatype_sort_num_constructors
  n_get_datatype_sort_recognizer
  n_get_decl_ast_parameter
  n_get_decl_double_parameter
  n_get_decl_func_decl_parameter
  n_get_decl_int_parameter
  n_get_decl_kind
  n_get_decl_name
  n_get_decl_num_parameters
  n_get_decl_parameter_kind
  n_get_decl_rational_parameter
  n_get_decl_sort_parameter
  n_get_decl_symbol_parameter
  n_get_domain
  n_get_domain_size
  n_get_full_version
  n_get_func_decl_id
  n_get_range
  n_get_sort
  n_get_sort_id
  n_get_sort_kind
  n_get_sort_name
  n_get_symbol_int
  n_get_symbol_kind
  n_get_symbol_string
  n_get_tuple_sort_mk_decl
  n_get_version
  n_is_as_array
  n_is_eq_func_decl
  n_is_eq_sort
  n_is_null_ast
  n_is_null_func_interp
  n_is_null_model
  n_is_numeral_ast
  n_is_well_sorted
  n_mk_add
  n_mk_and
  n_mk_app
  n_mk_ast_map
  n_mk_ast_vector
  n_mk_bool_sort
  n_mk_config
  n_mk_const
  n_mk_constructor_bytecode
  n_mk_context_rc
  n_mk_datatype
  n_mk_div
  n_mk_eq
  n_mk_false
  n_mk_fresh_const
  n_mk_fresh_func_decl
  n_mk_func_decl
  n_mk_ge
  n_mk_gt
  n_mk_implies
  n_mk_int
  n_mk_int_sort
  n_mk_le
  n_mk_lt
  n_mk_mul
  n_mk_not
  n_mk_null_ast
  n_mk_numeral
  n_mk_or
  n_mk_params
  n_mk_rec_func_decl
  n_mk_solver
  n_mk_string_symbol
  n_mk_sub
  n_mk_true
  n_mk_tuple_sort
  n_mk_uninterpreted_sort
  n_mk_xor
  n_model_get_const_decl
  n_model_get_const_interp
  n_model_get_func_decl
  n_model_get_func_interp
  n_model_get_num_consts
  n_model_get_num_funcs
  n_param_descrs_get_kind
  n_param_descrs_get_name
  n_param_descrs_size
  n_param_descrs_to_string
  n_params_set_bool
  n_params_set_double
  n_params_set_symbol
  n_params_set_uint
  n_params_to_string
  n_params_validate
  n_set_ast_print_mode
  n_set_internal_error_handler
  n_set_param_value
  n_simplify
  n_simplify_ex
  n_simplify_get_help
  n_simplify_get_param_descrs
  n_solver_assert
  n_solver_check
  n_solver_get_model
  n_sort_to_string
  n_substitute
  n_substitute_vars
  n_translate
  n_update_param_value
  n_update_term

All of these errors are linked to the use of Z3's OCaml bindings, which can't obviously work in Javascript since Z3 is made with C++.

The solution

A solution is simply to remove the use of the Z3 backend from Catala's proof platform when compiling to Javascript. For that, we need dune to express some form of conditional compilation paired with annotations in the code to remove completely the dependency on z3 when compiling to Javascript.

[AltGr]

Note: #223 will provide a workaround for this, but is not a perfect solution, since you'll have to choose between compiling with z3 support but without the js backend, or the opposite: only one version of the lib can be compiled at a time, with or without z3.

[denismerigoux]

Closed wuth #223