search

PrincetonUniversity / VST

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

Change the setting of INSTALLDIR. #644

Closed txyyss closed 1 year ago

txyyss commented 1 year ago

Set INSTALLDIR to the default one if ARCH is native.

andrew-appel commented 1 year ago

This looks good to me. I suggest you put this comment into the Makefile at line 230:

#  1. (if present) the VST installation for reasoning about 64-bit-mode C programs on the host 
#         architecture will be in $(COQLIB)/user-contrib/VST, 
#  2. (if present) the VST installation for reasoning about 32-bit-mode C programs for the 32-bit analogue
#       of the host architecture will be in $(COQLIB)/../coq-variant/VST32/VST
#  3. (if present) a VST installation for reasoning about C programs compiled for a _different_ 
#        architecture will be in $(COQLIB)/../coq-variant/VST_otherarch_bitsize/VST
#  Not all of this logic is right here in this makefile; some of it is done in the CompCert install,
#  in choosing how to configure CompCert itself, creating the values of $(ARCH) and $(BITSIZE)
MSoegtropIMC commented 1 year ago

Possibly one could change IS_ARM and IS_X86 to BOTH_ARM and BOTH_X86 since the logic is not that easy to understand.

andrew-appel commented 1 year ago

I will go ahead and make these changes now.