minor error messages building for 64 bit
dnaumann opened this issue · 2 comments
dnaumann commented
In the current master branch, using Install Method 3, make BITSIZE=64 builds a working system but there are a couple of error messages FWIW:
sh util/make_version 64
date: illegal option -- -
usage: date [-jnRu] [-d dst] [-r seconds] [-t west] [-v[+|-]val[ymwdHMS]] ...
[-f fmt date | [[[mm]dd]HH]MM[[cc]yy][.ss]] [+format]
COQC floyd/find_nth_tactic.v
util/coqflags: line 25: [: -v: unary operator expected
This is on macOS. Below is a transcript. It's for commit f10a9c4... but I saw the same errors from commits a few days ago.
~/repos/VST>make BITSIZE=64 -j7
===== CONFIGURATION SUMMARY =====
COMPCERT=platform
COMPCERT_SRC_DIR=__NONE__
COMPCERT_INST_DIR=/Users/naumann/.opam/_coq-platform_.2021.02.0/lib/coq/user-contrib/compcert
BITSIZE=64
ARCH=x86
INSTALLDIR=/Users/naumann/.opam/_coq-platform_.2021.02.0/lib/coq/user-contrib/VST
===== DERIVED CONFIGURATION =====
COMPCERT_INFO_PATH_REF=compcert
COMPCERT_EXPLICIT_PATH=false
COMPCERT_BUILD_FROM_SRC=false
COMPCERT_NEW=false
COQFLAGS= -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox
COMPCERT_R_FLAGS=
=================================
Makefile:872: .depend: No such file or directory
coqdep ... >.depend
# DEPENDENCIES DEFAULT
coqdep -vos -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox 2>&1 >.depend `find msl sepcomp veric floyd progs64 concurrency atomics wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox -name "*.v"` | grep -v 'Warning:.*found in the loadpath' || true
wc .depend
2397 22133 605771 .depend
===== CONFIGURATION SUMMARY =====
COMPCERT=platform
COMPCERT_SRC_DIR=__NONE__
COMPCERT_INST_DIR=/Users/naumann/.opam/_coq-platform_.2021.02.0/lib/coq/user-contrib/compcert
BITSIZE=64
ARCH=x86
INSTALLDIR=/Users/naumann/.opam/_coq-platform_.2021.02.0/lib/coq/user-contrib/VST
===== DERIVED CONFIGURATION =====
COMPCERT_INFO_PATH_REF=compcert
COMPCERT_EXPLICIT_PATH=false
COMPCERT_BUILD_FROM_SRC=false
COMPCERT_NEW=false
COQFLAGS= -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox
COMPCERT_R_FLAGS=
=================================
echo -Q msl VST.msl -Q sepcomp VST.sepcomp -Q veric VST.veric -Q floyd VST.floyd -Q progs64 VST.progs64 -Q concurrency VST.concurrency -Q atomics VST.atomics -Q wand_demo wand_demo -Q sha sha -Q hmacfcf hmacfcf -Q tweetnacl20140427 tweetnacl20140427 -Q hmacdrbg hmacdrbg -Q aes aes -Q mailbox mailbox > _CoqProject
COQC msl/Axioms.v
util/coqflags > _CoqProject-export
COQC msl/simple_CCC.v
COQC veric/lift.v
COQC sepcomp/extspec.v
COQC floyd/sublist.v
Sh util/make_version 64
date: illegal option -- -
usage: date [-jnRu] [-d dst] [-r seconds] [-t west] [-v[+|-]val[ymwdHMS]] ...
[-f fmt date | [[[mm]dd]HH]MM[[cc]yy][.ss]] [+format]
COQC floyd/find_nth_tactic.v
util/coqflags: line 25: [: -v: unary operator expected
COQC floyd/computable_theorems.v
[no further errors]
MSoegtropIMC commented
@dnaumann : I guess you are on macOS? sorry, I just saw in your issue text that you are on macOS
andrew-appel commented
I cannot reproduce this today in MacOS: no error message, and the appropriate output from coqflags.
Also, the coqflags utility is much less important now that most users are installing via the Coq Platform, and VST is in the standard place in user-contrib.