Commit 991545d1 authored by Andrei Paskevich's avatar Andrei Paskevich

sanitize filenames generated by Driver

parent 28ed3730
......@@ -4,7 +4,7 @@
<file name="../my_cosine.why" verified="false" expanded="true">
<theory name="CosineSingle" verified="false" expanded="true">
<goal name="MethodError" sum="03308e96177082a1d3da02e1d9af1b90" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="my_cosine.why_CosineSingle_MethodError_1.v" obsolete="false">
<proof prover="coq" timelimit="2" edited="my_cosine_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="3.93"/>
</proof>
</goal>
......
......@@ -4,7 +4,7 @@
<file name="../decrease1.mlw" verified="true" expanded="true">
<theory name="Decrease1" verified="true" expanded="true">
<goal name="decrease1_induction" sum="eb0923143934165c0f02dda5dd1d9064" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="decrease1.mlw_Decrease1_decrease1_induction_2.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="decrease1_Decrease1_decrease1_induction_2.v" obsolete="false">
<result status="valid" time="0.74"/>
</proof>
</goal>
......
......@@ -60,12 +60,12 @@
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.3" expl="for loop preservation" sum="3aa1af1a36f6d647b47b87fbbf9c36d5" proved="true" expanded="false">
<proof prover="coq" timelimit="10" edited="insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_1.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="insertion_sort_InsertionSort_WP_parameter_insertion_sort_1.v" obsolete="false">
<result status="valid" time="0.56"/>
</proof>
</goal>
<goal name="WP_parameter insertion_sort.3.7.4" expl="for loop preservation" sum="25e0f93b5176e5c428dd7ef607364586" proved="false" expanded="true">
<proof prover="coq" timelimit="20" edited="insertion_sort.mlw_InsertionSort_WP_parameter insertion_sort_2.v" obsolete="false"><undone/>
<proof prover="coq" timelimit="20" edited="insertion_sort_InsertionSort_WP_parameter_insertion_sort_2.v" obsolete="false"><undone/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
......
......@@ -24,12 +24,12 @@
</proof>
</goal>
<goal name="frame_list" sum="bb671f60ef471cba398e52a876544a54" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_1.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="list_rev_M2_frame_list_1.v" obsolete="false">
<result status="valid" time="0.50"/>
</proof>
</goal>
<goal name="frame_list_ft" sum="d0c0dd407e6667c967cd37f14169af5e" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_list_ft_1.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="list_rev_M2_frame_list_ft_1.v" obsolete="false">
<result status="valid" time="0.54"/>
</proof>
</goal>
......@@ -49,7 +49,7 @@
</proof>
</goal>
<goal name="frame_model" sum="d5fd36bbd6e0e2aebeea5703bbf7b4d7" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="list_rev.mlw_M2_frame_model_1.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="list_rev_M2_frame_model_1.v" obsolete="false">
<result status="valid" time="0.53"/>
</proof>
</goal>
......
......@@ -6,7 +6,7 @@
<goal name="WP_parameter my_cosine" expl="correctness of parameter my_cosine" sum="dd173c4f589edbafa4fba6e5a9ea3037" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter my_cosine.1" expl="assertion" sum="42f9206597da619fa67e4871bf991914" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="my_cosine.mlw_M_WP_parameter my_cosine_1.v" obsolete="false">
<proof prover="coq" timelimit="2" edited="my_cosine_M_WP_parameter_my_cosine_1.v" obsolete="false">
<result status="valid" time="4.07"/>
</proof>
</goal>
......
......@@ -15,17 +15,17 @@
</proof>
</goal>
<goal name="Power_sum" sum="0222179599018e583f47a3d214f2e604" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_sum_1.v" obsolete="false">
<proof prover="coq" timelimit="2" edited="power_Power_Power_sum_1.v" obsolete="false">
<result status="valid" time="0.46"/>
</proof>
</goal>
<goal name="Power_mult" sum="9d09d633adb75294ad19c24d7ad24bf4" proved="true" expanded="true">
<proof prover="coq" timelimit="2" edited="power.mlw_Power_Power_mult_1.v" obsolete="false">
<proof prover="coq" timelimit="2" edited="power_Power_Power_mult_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
<goal name="Power_mult2" sum="c37356cfaed29d43e8813ffc76d4ea37" proved="true" expanded="true">
<proof prover="coq" timelimit="5" edited="power.mlw_Power_Power_mult2_1.v" obsolete="false">
<proof prover="coq" timelimit="5" edited="power_Power_Power_mult2_1.v" obsolete="false">
<result status="valid" time="0.52"/>
</proof>
</goal>
......
......@@ -33,7 +33,7 @@
</proof>
</goal>
<goal name="WP_parameter max_sum.3.4" expl="for loop preservation" sum="b29b56c4f850b63d6e5079f2ca902ea3" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="vstte10_max_sum.mlw_MaxAndSum_WP_parameter max_sum_1.v" obsolete="false">
<proof prover="coq" timelimit="10" edited="vstte10_max_sum_MaxAndSum_WP_parameter_max_sum_1.v" obsolete="false">
<result status="valid" time="0.48"/>
</proof>
</goal>
......@@ -98,7 +98,7 @@
</proof>
</goal>
<goal name="WP_parameter max_sum.3.6" expl="for loop preservation" sum="9eced79ed776df7a79ced48b49e04faf" proved="true" expanded="true">
<proof prover="coq" timelimit="20" edited="vstte10_max_sum.mlw_MaxAndSum2_WP_parameter max_sum_3.v" obsolete="false">
<proof prover="coq" timelimit="20" edited="vstte10_max_sum_MaxAndSum2_WP_parameter_max_sum_3.v" obsolete="false">
<result status="valid" time="0.47"/>
</proof>
</goal>
......
......@@ -39,7 +39,7 @@
</proof>
</goal>
<goal name="solution_eq_board" sum="b9d1019b6d99c0a051ebcaaa83115667" proved="true" expanded="true">
<proof prover="coq" timelimit="20" edited="vstte10_queens.mlw_NQueens_solution_eq_board_1.v" obsolete="false">
<proof prover="coq" timelimit="20" edited="vstte10_queens_NQueens_solution_eq_board_1.v" obsolete="false">
<result status="valid" time="0.60"/>
</proof>
</goal>
......
......@@ -53,12 +53,12 @@
</proof>
</goal>
<goal name="WP_parameter search_loop.4.3" expl="correctness of parameter search_loop" sum="4c9df428be6e041e1b2ed5ddb9cfb1e4" proved="true" expanded="true">
<proof prover="coq" timelimit="20" edited="vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_2.v" obsolete="false">
<proof prover="coq" timelimit="20" edited="vstte10_search_list_SearchingALinkedList_WP_parameter_search_loop_2.v" obsolete="false">
<result status="valid" time="0.57"/>
</proof>
</goal>
<goal name="WP_parameter search_loop.4.4" expl="correctness of parameter search_loop" sum="8e048cf7dd305548e46d0c0624828372" proved="true" expanded="true">
<proof prover="coq" timelimit="20" edited="vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_3.v" obsolete="false">
<proof prover="coq" timelimit="20" edited="vstte10_search_list_SearchingALinkedList_WP_parameter_search_loop_3.v" obsolete="false">
<result status="valid" time="0.68"/>
</proof>
</goal>
......@@ -79,7 +79,7 @@
</transf>
</goal>
<goal name="WP_parameter search_loop.6" expl="normal postcondition" sum="d01b1212c0ab3708ed70ad837bb1929c" proved="true" expanded="true">
<proof prover="coq" timelimit="20" edited="vstte10_search_list.mlw_SearchingALinkedList_WP_parameter search_loop_4.v" obsolete="false">
<proof prover="coq" timelimit="20" edited="vstte10_search_list_SearchingALinkedList_WP_parameter_search_loop_4.v" obsolete="false">
<result status="valid" time="0.63"/>
</proof>
</goal>
......
......@@ -204,15 +204,17 @@ exception UnknownSpec of string
let filename_regexp = Str.regexp "%\\(.\\)"
let get_filename drv input_file theory_name goal_name =
let sanitize = Ident.sanitizer
Ident.char_to_alnumus Ident.char_to_alnumus in
let file = match drv.drv_filename with
| Some f -> f
| None -> "%f-%t-%g.dump"
in
let replace s = match Str.matched_group 1 s with
| "%" -> "%"
| "f" -> input_file
| "t" -> theory_name
| "g" -> goal_name
| "f" -> sanitize input_file
| "t" -> sanitize theory_name
| "g" -> sanitize goal_name
| s -> raise (UnknownSpec s)
in
Str.global_substitute filename_regexp replace file
......
......@@ -1649,12 +1649,9 @@ let transform ~context_unproved_goals_only tr a =
let ft_of_th th =
(Filename.basename th.theory_parent.file_name,
(*
th.theory.Theory.th_name.Ident.id_string
*)
th.theory_name
)
let fn = Filename.basename th.theory_parent.file_name in
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
(fn, (* th.theory.Theory.th_name.Ident.id_string *) th.theory_name)
let rec ft_of_goal g =
match g.parent with
......@@ -1685,9 +1682,8 @@ let edit_proof ~default_editor ~project_dir a =
match a.edited_as with
| "" ->
let (fn,tn) = ft_of_pa a in
let file = Driver.file_of_task driver
(Filename.concat project_dir fn) tn t
in
let file = Driver.file_of_task driver fn tn t in
let file = Filename.concat project_dir file in
(* Uniquify the filename if it exists on disk *)
let i =
try String.rindex file '.'
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment