1818DOWNLOADS_DIR = "downloads"
1919RESULTS_DIR = "reports/results"
2020
21- PRESET_PROJECTS = {
22- "flocq" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/fcoq/flocq" ,
23- "sha" :"afa04b781439bdc8e7b64580ce5227057fe706f1" ,
24- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
25- "qdir" :"" ,
26- "rdir" :"src,Flocq" },
27- "structtact" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/coq-mutation/structtact" ,
28- "sha" :"5c54c0389d081993232292f132e876ae812f04ca" ,
29- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
30- "qdir" :".,StructTact" ,
31- "rdir" :"" },
32- "prettyparsing" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/coq-mutation/prettyparsing" ,
33- "sha" :"f060ceae6c85d24439ae321bf2c3bd5d805d8a70" ,
34- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
35- "qdir" :".,PrettyParsing" ,
36- "rdir" :"" },
37- "tlc" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/fcoq/tlc" ,
38- "sha" :"103ffa6d00ec685d242fa27abf53e801b184f711" ,
39- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
40- "qdir" :"" ,
41- "rdir" :"src,TLC" },
42- "stdpp" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/fcoq/stdpp" ,
43- "sha" :"c3ecf18aa9a57f7b3232751032d8de3eecb09ce6" ,
44- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
45- "qdir" :"theories,stdpp" ,
46- "rdir" :"" },
47- "qarithsternbrocot" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/coq-mutation/qarithsternbrocot" ,
48- "sha" :"c27a584414f997268265ec612621bb083368f81e" ,
49- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
50- "qdir" :"" ,
51- "rdir" :".,QArithSternBrocot" },
52- "huffman" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/coq-mutation/huffman" ,
53- "sha" :"c5610a9c5839157c6d607e674a27949efccbfd14" ,
54- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
55- "qdir" :"" ,
56- "rdir" :".,Huffman" },
57- "quicksortcomplexity" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/coq-mutation/quicksortcomplexity" ,
58- "sha" :"38efe42d89498a4edddaf1269df5173c62713f46" ,
59- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
60- "qdir" :"" ,
61- "rdir" :".,QuicksortComplexity" },
62- "stalmarck" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/coq-mutation/stalmarck" ,
63- "sha" :"8ddb07034d13337969a8049334a07e5ac1402bf3" ,
64- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
65- "qdir" :"" ,
66- "rdir" :".,Stalmarck" },
67- "atbr" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/fcoq/atbr" ,
68- "sha" :"bb14340a9e8c3cde47a4b51fe530a669f915b647" ,
69- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
70- "qdir" :"" ,
71- "rdir" :"theories,ATBR" },
72- "fcslpcm" : {"url" : "https://github.com/imdea-software/fcsl-pcm" ,
73- "sha" :"eef45034808487fa3fa7dc360514c6734efc8d07" ,
74- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
75- "qdir" :"" ,
76- "rdir" :".,fcsl" },
77- "mathcomp" : {
"url" :
"ssh://[email protected] :2002//home/repos/projects/fcoq/mathcomp" ,
78- "sha" :"d9b349fbd3c2e73182b91b972425fff4fa774d25" ,
79- "buildcmd" : "coq_makefile -f _CoqProject -o Makefile; make -j8" ,
80- "qdir" :"" ,
81- "rdir" :".,mathcomp" }
82- }
83-
8421def setup_repo ():
8522 curr_dir = os .getcwd ()
8623 if not os .path .exists (DOWNLOADS_DIR ):
@@ -156,15 +93,13 @@ def get_results(command, mcoq_mode):
15693
15794def check_args ():
15895 global args
159- IS_CUSTOM_MODE = not "--preset" in sys .argv
16096 parser = argparse .ArgumentParser ()
16197 parser .add_argument ('--project' , help = 'project to run report on' , required = True )
16298 parser .add_argument ('--nocheck' , help = 'skip checking dependencies' , action = 'store_true' , default = False )
163- parser .add_argument ('--preset' , help = 'run prexisting project in paper' , action = 'store_true' , default = False )
164- parser .add_argument ('--sha' , help = 'sha of defined project' , required = IS_CUSTOM_MODE )
99+ parser .add_argument ('--sha' , help = 'sha of defined project' , required = True )
165100 parser .add_argument ('--report_dir' , help = 'directory to generate reports in' , default = '' )
166- parser .add_argument ('--buildcmd' , help = 'coq build command' , required = IS_CUSTOM_MODE )
167- parser .add_argument ('--url' , help = 'url to clone project' , required = IS_CUSTOM_MODE )
101+ parser .add_argument ('--buildcmd' , help = 'coq build command' , required = True )
102+ parser .add_argument ('--url' , help = 'url to clone project' , required = True )
168103 parser .add_argument ('--rdir' , help = 'rdir for coq. Colon separated list that becomes coq rflags. For example .,StructTact:.,fcsl becomes --rflag .,StructTact --rflag .,fcsl' , default = "" )
169104 parser .add_argument ('--qdir' , help = 'qdir for coq. Colon separated list that becomes coq flags. For example .,StructTact:.,fcsl becomes --flag .,StructTact --flag .,fcsl' , default = "" )
170105 parser .add_argument ('--skipeq' , help = 'skip equivelant mutants' , default = False , action = 'store_true' )
@@ -180,25 +115,10 @@ def check_args():
180115 except :
181116 print ("ERROR: Missing required arguments. Please ensure you have passed correct arguments. List of required args shown above." )
182117 return False
183-
184- # if args.threads != "" and not args.skipreport:
185- # print("ERROR: To run with multiple threads, must pass in the skipreport flag. Cannot run multiple threads and report.")
186- # return False
187118
188- if IS_CUSTOM_MODE and args .qdir == "" and args .rdir == "" :
119+ if args .qdir == "" and args .rdir == "" :
189120 print ("ERROR: Missing required arguments qdir/rdir. You need to specify one of these two arguments." )
190121 return False
191-
192- if args .preset :
193- if not (args .project in PRESET_PROJECTS ):
194- print ("ERROR: Supplied incorrect name for preset project" )
195- return False
196- project_data = PRESET_PROJECTS [args .project ]
197- args .sha = project_data ["sha" ]
198- args .qdir = project_data ["qdir" ]
199- args .rdir = project_data ["rdir" ]
200- args .url = project_data ["url" ]
201- args .buildcmd = project_data ["buildcmd" ]
202122
203123 return True
204124
@@ -249,14 +169,6 @@ def check_dependencies():
249169 return False
250170 return True
251171
252- def check_preset_dependencies ():
253- if args .project == "prettyparsing" :
254- check_opam_dependency ("coq-struct-tact" , "prettyparsing" )
255- if args .project == "atbr" :
256- check_opam_dependency ("atbr-plugin" , "atbr" )
257- if args .project == "mathcomp" :
258- check_opam_dependency ("coq-mathcomp-ssreflect" , "mathcomp" )
259-
260172def check_opam_dependency (package , project ):
261173 opam_check = check_command ("opam list" , package )
262174 if not opam_check :
@@ -310,8 +222,6 @@ def main():
310222 if os .path .exists (OLD_REPORT_DIR + "/mcoq_log.txt" ):
311223 os .system ("rm -rf " + OLD_REPORT_DIR + "/mcoq_log.txt" )
312224
313- if args .preset :
314- check_preset_dependencies ()
315225 if not args .skipmutations :
316226 setup_repo ()
317227 run_java (MCOQ_MODE )
@@ -325,12 +235,8 @@ def main():
325235 print ("Error running mcoq script. Exiting now." )
326236
327237# General examples for running mcoq.py
328- # (any custom project - min params) - ./mcoq.py --project [PROJECT NAME] --sha [PROJECT SHA] --url [PROJECT URL] --buildcmd [PROJECT CMD] --qdir [PROJECT QDIR] --rdir [PROJECT RDIR]
329- # (any preset project - min params) - ./mcoq.py --project [PROJECT NAME] --preset
330-
331- # Specifc examples for running mcoq.py
332- # structtact (custom) - ./mcoq.py --project structtact --sha 5c54c0389d081993232292f132e876ae812f04ca --url "ssh://[email protected] :2002//home/repos/projects/coq-mutation/structtact" --buildcmd "coq_makefile -f _CoqProject -o Makefile; make -j8" --qdir ".,StructTact" 333- # structtact (preset) - ./mcoq.py --project structtact --preset
334- # prettyparsing (preset) - ./mcoq.py --project prettyparsing --preset
238+ # ./mcoq.py --project [PROJECT NAME] --sha [PROJECT SHA] --url [PROJECT URL] --buildcmd [PROJECT CMD] --qdir [PROJECT QDIR] --rdir [PROJECT RDIR]
335239
240+ # Specific examples for running mcoq.py
241+ # structtact - ./mcoq.py --project StructTact --sha 82a85b7ec07e71fa6b30cfc05f6a7bfb09ef2510 --url https://github.com/uwplse/StructTact.git --buildcmd "./configure && make -j4" --qdir ".,StructTact"
336242# To see list of all arguments type ./mcoq.py --help
0 commit comments