PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

`make install` fails with "install: cannot stat 'msl/LICENSE': No such file or directory" #704

Closed JasonGross closed 10 months ago

JasonGross commented 10 months ago
$ make "IGNORECOQVERSION=true" "IGNORECOMPCERTVERSION=true" "ZLIST=platform" "BITSIZE=64" install
===== CONFIGURATION SUMMARY =====
COMPCERT=platform
COMPCERT_SRC_DIR=__NONE__
COMPCERT_INST_DIR=/home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/compcert
ZLIST=platform
BITSIZE=64
ARCH=x86
INSTALLDIR=/home/jgross/.local64/coq/coq-master/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=
=================================
install -d "/home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/VST"
for d in ./ doc/ msl/; do install -d "/home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/VST/$d"; done
for f in ; do install -m 0644 $f "/home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/VST/$(dirname $f)"; done
for f in LICENSE HISTORY CHANGES README.md VERSION msl/CREDITS msl/EXTRACTION msl/LICENSE msl/README.html msl/SUMMARY doc/VC.pdf VST.config; do install -m 0644 $f "/home/jgross/.local64/coq/coq-master/lib/coq/user-contrib/VST/$(dirname $f)"; done
install: cannot stat 'msl/LICENSE': No such file or directory

Seems to have been removed in b88da7af666299725050ee8ec411cbedeb85dc94