@@ -34,7 +34,8 @@ output_path=$3
3434output_dir=$( dirname " $output_path " )
3535[ -d " $output_dir " ] || mkdir -p " $output_dir "
3636
37- export HOLLIGHT_DIR=" $( dirname ${hol_sh_cmd} ) "
37+ HOLLIGHT_DIR=" $( dirname " ${hol_sh_cmd} " ) "
38+ export HOLLIGHT_DIR
3839if [ ! -f " ${HOLLIGHT_DIR} /hol_lib.cmxa" ]; then
3940 echo " hol_lib.cmxa does not exist in HOLLIGHT_DIR('${HOLLIGHT_DIR} ')."
4041 echo " Did you compile HOL Light with HOLLIGHT_USE_MODULE set to 1?"
@@ -50,20 +51,20 @@ echo "Generating a template .ml that loads the file...: ${template_ml}"
5051 echo " check_axioms ();;"
5152 echo ' let proof_end_time = Unix.time();;'
5253 echo ' Printf.printf "Running time: %f sec, Start unixtime: %f, End unixtime: %f\n" (proof_end_time -. proof_start_time) proof_start_time proof_end_time;;'
53- ) >> ${template_ml}
54+ ) >> " ${template_ml} "
5455
5556inlined_prefix=" $( mktemp) "
5657inlined_ml=" ${inlined_prefix} .ml"
5758inlined_cmx=" ${inlined_prefix} .cmx"
58- (cd " ${S2N_BIGNUM_DIR} " && HOLLIGHT_LOAD_PATH=${ROOT} ocaml ${HOLLIGHT_DIR} /inline_load.ml " ${template_ml} " " ${inlined_ml} " )
59+ (cd " ${S2N_BIGNUM_DIR} " && HOLLIGHT_LOAD_PATH=${ROOT} ocaml " ${HOLLIGHT_DIR} " /inline_load.ml " ${template_ml} " " ${inlined_ml} " )
5960
6061# Give a large stack size.
6162OCAMLRUNPARAM=l=2000000000 \
6263 ocamlopt.byte -pp " $( ${hol_sh_cmd} -pp) " -I " ${HOLLIGHT_DIR} " -I +unix -c \
63- hol_lib.cmxa ${inlined_ml} -o ${inlined_cmx} -w -a
64+ hol_lib.cmxa " ${inlined_ml} " -o " ${inlined_cmx} " -w -a
6465ocamlfind ocamlopt -package zarith,unix -linkpkg hol_lib.cmxa \
65- -I " ${HOLLIGHT_DIR} " ${inlined_cmx} \
66+ -I " ${HOLLIGHT_DIR} " " ${inlined_cmx} " \
6667 -o " ${output_path} "
6768
6869# Remove the intermediate files to save disk space
69- rm -f ${inlined_cmx} ${template_ml} ${inlined_ml}
70+ rm -f " ${inlined_cmx} " " ${template_ml} " " ${inlined_ml} "
0 commit comments