Stream: Coq Platform devs & users

Topic: Meaning of `-pick` suffixes?

Paolo Giarrusso (Dec 02 2021 at 20:35):

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)?

Paolo Giarrusso (Dec 02 2021 at 21:28):

Edited — I first tried -pick=1 since 1 is the answer I give to the wizard, and that scheme works for all other options.

Michael Soegtrop (Dec 03 2021 at 13:48):

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.

Michael Soegtrop (Dec 03 2021 at 13:49):

Maybe it would make sense to print out the complete command line after all questions. Something like "to rerun with the same options ...".

Paolo Giarrusso (Dec 03 2021 at 14:16):

"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).

Michael Soegtrop (Dec 03 2021 at 14:34):

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.

Paolo Giarrusso (Dec 03 2021 at 14:54):

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