{"push_id":2647476477,"size":1,"distinct_size":1,"ref":"refs/heads/gpl-2018","head":"f956f58fb70dae026b700611502f02615f3c2154","before":"3cfd67b06488bfc9bc21587cc2549239e9ee1467","commits":[{"sha":"f956f58fb70dae026b700611502f02615f3c2154","author":{"name":"Johannes Kanig","email":"983a57481bbfdc6b23ae3d5719223d365cdf5733@adacore.com"},"message":"Updated git submodules\n\nProject: why3 master b17873a181ff56abda9d09bc8d10c29ba036c019\n\nR531-011 implement killing of tasks\n\nThe why3server supports the \"interrupt\" command which removes a task.\nBut until now, the server didn't actually kill any already running\nprocesses. This is now implemented.\n\nBackground is that I plan some refactorings which may make use of the\n\"interrupt\" command, so I want it to work properly.\n\nThis new code is untested on windows, because no client code actually\nuses the interrupt command in SPARK. But I tested that it doesn't cause\nregressions. It will be later tested by the new code I intend to write.\n\n*server-unix.c\n*server-win.c\n(overall): outsource some little code to new proc unit\n(handle_msg): actually kill processes\n\n* proc.c - new file\n(os_kill): new platform-dependent function to kill a process by pid\n(init_process_list): new function to init the process list\n(kill_processes): new function to kill processes from process list with\n  a certain key\n(free_process): release memory held by a process record\n\nChange-Id: I7238578061c65883423f8ec538d79d9de3fb717b\n\n\nQ802-001 new VC kind VC_Inline_Check\n\nThis kind is used to check Inline_For_Proof annotations.\n\n* src/gnat/gnat_expl.ml\n(reason): New reason VC_Inline_Check.\n\nChange-Id: Ib806e9e786fc1a7478a7b12cbb57a64f1c16674c\n\n\nR508-015 Adapt the last merge commit\n\nThis updates the configure, changes the printing of labels to Json and\nconverts the following terminology:\n - Stdlib -> Wstdlib\n - split_goal_wp -> split_goal_right\n\nChange-Id: I0d4af3803f16c775817a60587c459630425e42c4\n\n\nR508-015 Mrge lri into adacore master\n\nThis commit intends to add printing of labels for counterexamples\nidentifiers: this helps for the if-branching for ce.\n\nConflcts:\n\tMakefile.in\n\tdrivers/cvc4_14.drv\n\tdrivers/cvc4_16_counterexample.drv\n\tsrc/transform/abstract_quantifiers.ml\n\tsrc/transform/eliminate_symbol.ml\n\nChange-Id: I2ff7c24282e4457c4996713beaed6fcfec608f24\n\n\nAdd customization of foreground colors for error messages.\n\nBlack on red was not readable. Colors to be decided.\n\n\ntactic apply: add appropriate exception. simplify code and allow inductive\n\nAs a side effect, this also modifies reflection.ml accordingly.\n\nConflicts:\n\tsrc/transform/reflection.ml\n\n\nAllow (again) applying transformation on proof attempt (apply on parent)\n\n\n(no-tn-check) use parallel constant to initialize lists\n\nChange-Id: I5c9202411fe46955c80a991eca2b7d5c2272f6d4\n(cherry picked from commit 1871023be2e4ec01bc413d4f2b670c2ed208a61a)\n\n\nR531-011 declare global queue in request module\n\nThis allows sharing of some code between unix and windows server\n\n* request.c\n(queue): move global variable here\n(init_request_queue): initialize global queue\n(remove_from_queue): moved here\n* server-unix.c\n(queue): remove global variable\n(server_init_listening): call init_request_queue\n(remove_from_queue): moved from here\n(handle_msg): change call to remove_from_queue, now without queue arg\n* server-win.c\n(queue): remove global variable\n(handle_msg): now call remove_from_queue\n(init): call init_request_queue\n\nChange-Id: I741b8f958a0678a7acdc0c40a3b6fa72f7fb7a2c\n(cherry picked from commit 77ff3c64d289cb8d3c845f52708fed9155ca49e1)\n\n\n(no-tn-check) more precise comment for list_remove\n\nChange-Id: I4645da26a36023a7c0c76afaa250783384b94ccd\n(cherry picked from commit fbeff2266782c47362cbe92513d23458c5c69788)\n\n\nR515-014 Adapt new cvc4 to ce\n\nThis commit adapts the changes made by Florian to the drivers of cvc4 for\ncounterexamples (for float with cvc4 version 1.6). It reuses without\nchanges the drivers he intended to use.\nI modified the model parser so that it can recognize float models of cvc4.\n\n* drivers/cvc4_16_counterexample.drv\nAdded import smt-libv2-floats.gen.\n\n* src/driver/parse_smtv2_model_lexer.mll\nAdded a token for float_type.\n\n* src/driver/parse_smtv2_model_parser.mly\nFloat_type can be encountered as names in the model but produce nothing.\n\n\nChange-Id: I64b49dd1824138a5d3f98ab046da0fdbc9420e66\n(cherry picked from commit 226d70801ad449fb86d73d35ac07fcfd56b8ba65)\n\nConflicts:\n\tdrivers/cvc4_15_counterexample.drv\n\tdrivers/cvc4_16_counterexample.drv\n\tdrivers/cvc4_gnatprove_ce.drv\n\n\nR518-009 fix unsoundness related to multiple handlers\n\nThere were two bugs in the Etry case for fastwp:\n\n- soundness issue: the case for the normal exit was wrong.  It tried to\n  merge the states iteratively by pairs, which is wrong. Instead, states\n  need to be merged at once. Given the traversal that was done, it wasn't\n  easily fixable, so a rewrite of the entire Etry case was necessary.\n- completeness issue: some information was dropped for the exceptional\n  exits. Some code is required to recover this information.\n\n* mlw_wp.ml\n(fast_wp_desc): fix Etry case\n\nChange-Id: Ic39045baa145b3933312f4d2499582a9251b2f6c\n(cherry picked from commit c50300b6f4aa193e008492a5af719ee03cd72211)\n\n\nRemove compilation warnings\n\n\nQ817-011 proof - use cvc4 for floats\n\nDriver updates and refactoring. Add new floats drivers file.\n\nAlso add Clément's old transformation (intended for colibri) for\nelimination of ident/types/etc.\n\nChange-Id: I161612592904ed3700b414c01ccab7944654d4d9\n(cherry picked from commit a82204236d1e73207dbd71b95236757d0eeacfa2)\n\nConflicts:\n\tdrivers/cvc4_14.drv\n\tdrivers/cvc4_15.drv\n\tdrivers/cvc4_gnatprove.drv\n\tdrivers/z3_gnatprove.drv\n\tdrivers/z3_gnatprove_ce.drv\n\n\nUpdate ce parser to accept empty model.\n\n\nWhen printing models, add labels associated to a model element name id\n\nThis way, (labels|tags|attributes) can be retrieved on counterexamples\nnames.\n\n\n(no-tn-check) use parallel constant to initialize lists\n\nChange-Id: I5c9202411fe46955c80a991eca2b7d5c2272f6d4\n\n\nR531-011 declare global queue in request module\n\nThis allows sharing of some code between unix and windows server\n\n* request.c\n(queue): move global variable here\n(init_request_queue): initialize global queue\n(remove_from_queue): moved here\n* server-unix.c\n(queue): remove global variable\n(server_init_listening): call init_request_queue\n(remove_from_queue): moved from here\n(handle_msg): change call to remove_from_queue, now without queue arg\n* server-win.c\n(queue): remove global variable\n(handle_msg): now call remove_from_queue\n(init): call init_request_queue\n\nChange-Id: I741b8f958a0678a7acdc0c40a3b6fa72f7fb7a2c\n\n\n(no-tn-check) more precise comment for list_remove\n\nChange-Id: I4645da26a36023a7c0c76afaa250783384b94ccd\n\n\ndisabled useless code for counterexamples\n\n\nfix CE test\n\n\n(no-tn-check) remove useless if\n\nThis test is always false, it is in the else-branch of an if with the\nsame test\n\nChange-Id: I998d8ec1fcdb0f5a0edf9b0ec803c5e9840b4e0e\n\n\nR529-004 add CONTRIBUTING.md\n\nChange-Id: I79d77484f3da231bef2efd6802a52f8e950cba82\n\n\nAvoid using kasprintf, which does not exist on OCaml 4.02.\n\n\nMerge branch 'next' into new_ide\n\n\nMerge branch 'bugfix/v0.88' into next\n\n\nPotentially install extra opam packages when testing, including packages for Coq.\n\n\nDo not compile with -j2, since the CI slaves have a single core.\n\n\nR515-014 Adapt new cvc4 to ce\n\nThis commit adapts the changes made by Florian to the drivers of cvc4 for\ncounterexamples. It reuses without changes the drivers he intended to use.\nI modified the model parser so that it can recognize float models of cvc4.\n\n* drivers/cvc4_15.drv\nRenamed into drivers/cvc4_16_counterexample.drv\n\n* drivers/cvc4_15_counterexample.drv\nRenamed into drivers/cvc4_gnatprove_ce.drv\n\n* drivers/cvc4_16_counterexample.drv\nAdded import smt-libv2-floats.gen.\n\n* drivers/cvc4_gnatprove_ce.drv\nAdded imports to cvc4_16_counterexample and adapted lib of float. Also,\nadded and commented theory int.ComputerDivision because it triggers\nregressions in counterexamples.\n\n* src/driver/parse_smtv2_model_lexer.mll\nAdded a token for float_type.\n\n* src/driver/parse_smtv2_model_parser.mly\nFloat_type can be encountered as names in the model but produce nothing.\n\n\nChange-Id: I64b49dd1824138a5d3f98ab046da0fdbc9420e66\n\n\nnew uninstalled prover policy is now taken into account in the next replay\n\nThere is no need to exit and restart IDE anymore\n\n\nCheck whether ocamlfind might have returned the actual location of nums.cma.\n\nThe standard install location of the num library is $OCAMLLIB. Thus, the\nanswer of ocamlfind cannot generally be trusted since it returns the\nlocation of the META file. Yet, on Arch Linux, nums.cma is actually stored\nnext to its META file, for some reason. So, this commit makes configure\ntry this location before falling back to the standard one.\n\n\nR518-009 fix unsoundness related to multiple handlers\n\nThere were two bugs in the Etry case for fastwp:\n\n- soundness issue: the case for the normal exit was wrong.  It tried to\n  merge the states iteratively by pairs, which is wrong. Instead, states\n  need to be merged at once. Given the traversal that was done, it wasn't\n  easily fixable, so a rewrite of the entire Etry case was necessary.\n- completeness issue: some information was dropped for the exceptional\n  exits. Some code is required to recover this information.\n\n* mlw_wp.ml\n(fast_wp_desc): fix Etry case\n\nChange-Id: Ic39045baa145b3933312f4d2499582a9251b2f6c\n\n\nMake some examples pass with Jessie.\n\n\nFix compilation of Jessie 3.\n\n\nAdd missing file.\n\n\nFix compilation of Jessie 3.\n\n\nImprove detection of Frama-C and add Merlin support.\n\n\nFix #119\n\nNodes that are detached now keep their former obsolete status\n\n(cherry picked from commit 7cb941bac8a22a7fe20e5c80703d408b17112e77)\n\n\nEscape goal names.\n\n\nEscape goal and transformation names.\n\n\nFix output of transformation arguments and factor some common code.\n\n\nMerge branch 'next' into new_ide\n\n\nRename Stdlib into Wstdlib (fix issue #105).\n\nOCaml 4.07 introduces a new standard module named Stdlib, which clashes\nwith the one from Why3 (during the compilation of Why3).\n\n\nMerge branch 'bugfix/v0.88' into next\n\n\nfix session\n\n\nMark Coq 8.8.0 as supported.\n\n\nImprove detection of installed packages.\n\nOn Debian, .cmi files might be missing, while META files are installed.\nThis confuses ocamlfind in believing development files are available.\nSo, we now systematically check that there is at least a .cmi file.\nThis also helps when ocamlfind is not present.\n\n\nSubstitute all the constants (fix issue #110).\n\n\nDisable tactic for Coq 8.8.\n\n\nPartly fix compilation with Coq 8.8.\n\n\nFix unbalanced output when a transformation has no subgoals.\n\n\nFix broken conditional and clean code.\n\n\nfixed subst and subst_all, close issue #16\n\n\nR511-024 Change model parsing for ce\n\nNow considers the end of the model as being the last set of parenthesis\n))) on beginning of line, not just a single one.\n\n* src/driver/parse_smtv2_model.ml\n(parse): Changed slightly the regexp used for end of model.\n\nChange-Id: I020d975e73e2430403b36bbd6beaeb9060a31668\n(cherry picked from commit 73abf2f41f1973c69814a2f6a3c0c6d77c83745a)\n\n\nfix obsolete session\n\n\nfix bench script\n\n\nupdate obsolete sessions\n\n\nremoved deprecated transformations split_*_wp\n\n\nfix typo\n\n\nrename split_intros_goal_wp into split_vc\n\n\nintroduce_premises does not introduce a meta anymore\n\n\nNwe versions of transformations subst and subst_all\n\n\nError message for correct prover in cmdline with bad arguments\n\n\nPut transformations \"subst\" and \"subst_all\" in a separate file\n\nIncidentally, move the local \"fold\" function of apply.ml into the general\nmodule Trans\n\n\nFix typo.\n\nSpotted by Franz Brauße.","distinct":true,"url":"https://api.github.com/repos/AdaCore/spark2014/commits/f956f58fb70dae026b700611502f02615f3c2154"}]}
{"actor":{"display_login":"adacore-bot"}}