-
Notifications
You must be signed in to change notification settings - Fork 9
/
Copy pathbuild_for_coq.py
47 lines (42 loc) · 2.48 KB
/
build_for_coq.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
#=======================================================================================#
# #
# rmem executable model #
# ===================== #
# #
# This file is: #
# #
# Copyright Shaked Flur, University of Cambridge 2017 #
# Copyright Susmit Sarkar, University of St Andrews 2014 #
# Copyright Peter Sewell, University of Cambridge 2014 #
# Copyright Dominic Mulligan, University of Cambridge (when this work was done) 2013 #
# #
# All rights reserved. #
# #
# It is part of the rmem tool, distributed under the 2-clause BSD licence in #
# LICENCE.txt. #
# #
#=======================================================================================#
from subprocess import call
files = [
"src_concurrency_model/MachineDefUtils",
"src_concurrency_model/MachineDefFreshIds",
"src_concurrency_model/MachineDefValue",
"src_concurrency_model/MachineDefTypes",
"src_concurrency_model/MachineDefInstructionSemantics",
"src_concurrency_model/MachineDefStorageSubsystem",
"src_concurrency_model/MachineDefThreadSubsystem",
"src_concurrency_model/MachineDefSystem",
"src_concurrency_model/MachineDefAxiomaticCore"
]
processed_files = []
coqc_command = ["coqc", "-require", "../../bitbucket/lem/coq-lib/coq_ext_lib_standard"]
for fname in files:
lem_command = ["../../bitbucket/lem/lem", "-coq", "-lib", "../../bitbucket/lem/library"]
fname_lem = fname + ".lem"
fname_coq = fname + ".v"
processed_files.append(fname_lem)
for p in processed_files:
lem_command.append(p)
call(lem_command)
coqc_command.append(fname_coq)
call(coqc_command)