To time the script I wanted to convert my answers to options, so I tried
time ./coq_platform_make.sh -extent=b -pick=1 -parallel=p -jobs=16. But
-pick=1 didn't work... I ended up reading the scripts and using
time ./coq_platform_make.sh -extent=b -pick=8.14~2021.11 -parallel=p -jobs=4.
Could the wizard display the suffix as well (or could the help document how suffixes work, but that seems worse)?
Edited — I first tried
1 is the answer I give to the wizard, and that scheme works for all other options.
As the -h help of the script says, the pick is either a pick file name (full path) or the suffix of a pick file. There is also an "example_coq_platform_make.sh" which shows this (with the old -packages, though).
I didn't support pick numbers, because this would be quite brittle.
Maybe it would make sense to print out the complete command line after all questions. Something like "to rerun with the same options ...".
"Rerun with the same option" is a good idea — I recall the RedHat install wizard offering such a thing (tho that one created a config file).
I have read the help text and the one in the wizard. I'm sure they're perfectly clear to you, but I'm trying to say that neither one mentions either what I want (
8.14~2021.11) or how to find out (
ls package_picks/package-pick-*|sed -re 's!package_picks/package-pick-(.*)\.sh!\1!' would work for me). A
-pick=list option would work.
Instead, all other questions also mention the option to use, which is very intuitive:
Install full (f), extended (x), base (b) or IDE (i)? (f/x/b/i/c=cancel).
Let me think about how to improve on that. In the end using e.g. "1" might make sense, but e.g. "6" would likely mean quite something else after an update.
How about listing the valid (known) picks if an invalid pick is given? And/or one could list the valid picks in the command line help.
One can btw. also specify an arbitrary pick file.
yeah I agree that
-pick=1 is a bad idea, I just want something discoverable, and all your proposals help :-)
Last updated: Jan 30 2023 at 11:03 UTC