search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
612 stars 132 forks source link

Merge dprot and protect #644

Open xrchz opened 5 years ago

xrchz commented 5 years ago

There are two Holmakefile functions that, from a user's perspective, serve the same purpose: namely, protect strings that contain spaces or other unusual characters from being split into multiple items or otherwise mistreated. protect protects a string from the OS shell and dprot protects a string from Holmake's tokenisation.

I suggest these functions be accessible under a unified name (protect) and the correct semantics inferred from context (whether the string appears as a shell command vs not). This should also mean protect covers usage in variable definitions (e.g., INCLUDES).

mn200 commented 5 years ago

I don't think context can be inferred because these functions can occur on the RHSes of arbitrary variable definitions which may then be used in different places.

xrchz commented 5 years ago

And I guess the expansion happens at variable definition time rather than use?

mn200 commented 5 years ago

Hmm. Good point. I think that in theory make is supposed to expand at time of use, but I'm not so sure Holmake does this.

xrchz commented 5 years ago

Make has two kinds of variable that differ in exactly this respect. https://www.gnu.org/software/make/manual/html_node/Flavors.html#Flavors

mn200 commented 5 years ago

Indeed.