• Sylvain Dailler's avatar
    Merge branch 'new_ide' into master · 7c901fd6
    Sylvain Dailler authored
    This intends to add improvements that were done in new_ide but not merged
    in master yet.
    In particular, this merges
    - the commit for interruption of provers in why3server.
    - several counterexamples improvements:
      * choice of pretty printing for float counterexamples
      * countereamples parsing of lowercase "lambda"
    - itp_server/controller_itp improvements:
      * error handling in itp_server (any_from_node_ID is now option)
      * reformating of controller_itp queues as record instead of tuples
      * choice to always give a new goal with the automatic function that gets
    next goal
    
    Conflicts:
    	bench/ce/algebraic_type_CVC4,1.5.oracle
    	bench/ce/algebraic_type_Z3,4.6.0.oracle
    	bench/ce/array_records_CVC4,1.5.oracle
    	bench/ce/array_records_Z3,4.6.0.oracle
    	bench/ce/arrays_CVC4,1.5.oracle
    	bench/ce/arrays_Z3,4.6.0.oracle
    	bench/ce/floats_CVC4,1.5.oracle
    	bench/ce/floats_Z3,4.6.0.oracle
    	bench/ce/if_decision_branch.mlw
    	bench/ce/if_decision_branch_CVC4,1.5.oracle
    	bench/ce/if_decision_branch_Z3,4.6.0.oracle
    	bench/ce/int.mlw
    	bench/ce/int32_CVC4,1.5.oracle
    	bench/ce/int32_Z3,4.6.0.oracle
    	bench/ce/int_CVC4,1.5.oracle
    	bench/ce/int_Z3,4.6.0.oracle
    	bench/ce/int_overflow_CVC4,1.5.oracle
    	bench/ce/int_overflow_Z3,4.6.0.oracle
    	bench/ce/jlamp0_CVC4,1.5.oracle
    	bench/ce/jlamp0_Z3,4.6.0.oracle
    	bench/ce/jlamp_array_CVC4,1.5.oracle
    	bench/ce/jlamp_array_Z3,4.6.0.oracle
    	bench/ce/jlamp_projections_CVC4,1.5.oracle
    	bench/ce/jlamp_projections_Z3,4.6.0.oracle
    	bench/ce/map_CVC4,1.5.oracle
    	bench/ce/map_Z3,4.6.0.oracle
    	bench/ce/real_CVC4,1.5.oracle
    	bench/ce/real_Z3,4.6.0.oracle
    	bench/ce/record_map_CVC4,1.5.oracle
    	bench/ce/record_map_Z3,4.6.0.oracle
    	bench/ce/records_CVC4,1.5.oracle
    	bench/ce/records_Z3,4.6.0.oracle
    	bench/ce/ref_CVC4,1.5.oracle
    	bench/ce/ref_Z3,4.6.0.oracle
    	bench/ce/simple_array_CVC4,1.5.oracle
    	bench/ce/simple_array_Z3,4.6.0.oracle
    	src/core/ident.ml
    	src/core/ident.mli
    	src/parser/parser.mly
    	src/printer/alt_ergo.ml
    	src/printer/smtv2.ml
    	src/session/itp_server.ml
    	src/transform/eval_match.ml
    	src/transform/intro_projections_counterexmp.ml
    	src/transform/intro_vc_vars_counterexmp.ml
    	src/whyml/mlw_wp.ml
    	tests/demo-itp.mlw
    7c901fd6