Aleksey Arens (Feb 12 2021 at 02:06): Aleksey Arens (Feb 12 2021 at 02:06):Hello. I'm trying to configure a Dune build for Coq to update the pkgsrc package to the newest Coq release version (8.13.0). The issue that I'm coming across lately is that of a fileset mismatches with the PLIST specs from previous versions, and also with the appearance of new categories in the .install files. What is the purpose of files from lib_root section?
Emilio Jesús Gallego Arias (Feb 12 2021 at 02:49):Hi @Aleksey Arens , excuse my unfamiliarity with pkgsrc; what is a PLIST file, what is the mismatch you see?
Files in the lib_root section are placed there so they are installed on lib as opposed to lib/pkg, as of today coq requires all files to go in `lib/coq this will be updated in the future.
Aleksey Arens (Feb 12 2021 at 02:57):Apparently, opam has issued a new spec (cf. https://opam.ocaml.org/doc/Manual.html), with additional fields, which weren't quite familiar to the native opam-installer adapter tool (cf. https://github.com/jaapb/opaline). I've worked around by patching locally. Currently, my question is whether the native binaries of coq should be stripped?
Aleksey Arens (Feb 12 2021 at 02:57):I also wonder, if there's a natural way to request dune to build either native + byte / native only / byte only.
Aleksey Arens (Feb 12 2021 at 02:59):Hello Emilio. I'm a bit concerned, since I'm seeing quite a number of files in lib_root under coq.install. For example, an excerpt from the lib_root section:
"_build/install/default/lib/coq/theories/Arith/Arith.v" {"coq/theories/Arith/Arith.v"}
"_build/install/default/lib/coq/theories/Arith/Arith.vo" {"coq/theories/Arith/Arith.vo"}
"_build/install/default/lib/coq/theories/Arith/Arith_base.v" {"coq/theories/Arith/Arith_base.v"}
"_build/install/default/lib/coq/theories/Arith/Arith_base.vo" {"coq/theories/Arith/Arith_base.vo"}
"_build/install/default/lib/coq/theories/Arith/Between.v" {"coq/theories/Arith/Between.v"}
"_build/install/default/lib/coq/theories/Arith/Between.vo" {"coq/theories/Arith/Between.vo"}
"_build/install/default/lib/coq/theories/Arith/Bool_nat.v" {"coq/theories/Arith/Bool_nat.v"}
This looks like a discrepancy, since those files -- their destination being $PREFIX/lib/coq -- must be under that lib section, yet they're under the lib_root.
Aleksey Arens (Feb 12 2021 at 03:04):Are you positive that coq 8.13.0 requires the installation into $PREFIX/lib/coq/ rather than into $PREFIX/lib?
This is the coq.install file that I'm seeing: https://pastebin.com/kJBEBbk6
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:14):Currently, my question is whether the native binaries of coq should be stripped?
They should be handled as the OCaml policy you have specifies, they are not special [debian I guess strips them]
I also wonder, if there's a natural way to request dune to build either native + byte / native only / byte only.
I am not expert on this area, likely there is way. What's the use case? If the ocaml compiler doesn't have native capabilities Dune will adapt automatically.
This looks like a discrepancy, since those files -- their destination being $PREFIX/lib/coq -- must be under that lib section, yet they're under the lib_root.
This is due to the policy I mentioned, for example, a Coq theory named foo, has to still go under lib/coq/foo, not lib/foo as you would expect, so we need to override it, do you know what I mean?
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:15):Are you positive that coq 8.13.0 requires the installation into $PREFIX/lib/coq/ rather than into $PREFIX/lib?
Yup, I am positive, tho you could tweak this for your lib and install in a different location, however in this case libs won't be accessible by default
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:15):Actually coq requires install of everything in $lib/coq/user-contrib, but the stdlib is an exceptio
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:16):exception, we could tweak it, but other packages must still install there
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:16):Also you have some space to tweak depending how do you call configure
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:17):So indeed you could map lib_root to something else, but I'm unsure what happens if $lib is different from $lib_root/coq
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:19):update: I've checked the code, indeed the invariant Coq's code has is $lib = $lib_root/coq, due to the way cmxs and vo files are handled
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:19):that's easy to tweak tho / patch if you want
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:20):Regarding distro and packages my view is that you should describe to us how would you like for things to work, and we'll be sure Coq is flexible enough as to accomodate your needs
Aleksey Arens (Feb 12 2021 at 03:29):Emilio Jesús Gallego Arias said:
Currently, my question is whether the native binaries of coq should be stripped?
They should be handled as the OCaml policy you have specifies, they are not special [debian I guess strips them]
Ok. Good to know. NetBSD also does, unless they're byte-code.
I also wonder, if there's a natural way to request dune to build either native + byte / native only / byte only.
I am not expert on this area, likely there is way. What's the use case? If the ocaml compiler doesn't have native capabilities Dune will adapt automatically.
The use case is that of a package build system having options to request native or bytecode builds set.
Thinking about it, I wonder, if dune tries to build in as many ways as possible / available on the system? I guess, if it is so, then after the build finishes, I could simply cherry-pick files appropriate to a particular build setup.
This looks like a discrepancy, since those files -- their destination being $PREFIX/lib/coq -- must be under that lib section, yet they're under the lib_root.
This is due to the policy I mentioned, for example, a Coq theory named foo, has to still go under
lib/coq/foo, notlib/fooas you would expect, so we need to override it, do you know what I mean?
I'm not sure I quite follow you here.
I wonder, if the presence of files under lib/foo is an anomaly in that particular build? Is this something that could possibly happen? It appears that the policy of previous versions was to use prefixed directory. Did the policy change? I'm OK if it did, but I would like to know for sure, since I need to ensure the correct package build.
Aleksey Arens (Feb 12 2021 at 03:32):I wish to track the intention of the upstream authors as closely as reasonably possible. Thus, I do not wish to adjust the lib_root, unless it'll be necessary to fix breakage in the Coq system. If Coq 8.13.0 authors' intention does indeed involve putting those aforementioned files under $PREFIX/lib rather than $PREFIX/lib/coq, then I welcome this decision; however, I'm also trying to ascertain if it has indeed been a conscious decision, and not a fluke in the build specs.
Aleksey Arens (Feb 12 2021 at 03:38):The ideal of packaging that I'm pursuing is to alter the package to the reasonable necessary minimum to accommodate the host system. This goes very much hand-in-hand along with the policy of pkgsrc. I appreciate the automation offered by dune, and only wish to be sure that it had auto-configured against the correct local environment. Similarly, I would like to see files under the directory structure that was seen as most appropriate by package's authors. Now, since some files were uder lib rather than lib_root in the previous release, I would like to understand why, and to be sure that nothing would get broken if I leave things as they are. I desire the least to change the directory layout within the package's domain.
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:38):Thinking about it, I wonder, if dune tries to build in as many ways as possible / available on the system? I guess, if it is so, then after the build finishes, I could simply cherry-pick files appropriate to a particular build setup.
I'm sure there is a better way, tho Coq doesn't make a lot of sense to be used as a bytecode [gets slow quick] , so indeed dune will try to use coqc native always to compile the stdlib, but we could tweak it.
Did the policy change?
Not sure I fully follow you here, but the file layout resulting from the current build should be identical than the previous ones.
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:39):Oh, no file should go under lib , all files go under lib/coq
Aleksey Arens (Feb 12 2021 at 03:39):Emilio Jesús Gallego Arias said:
Thinking about it, I wonder, if dune tries to build in as many ways as possible / available on the system? I guess, if it is so, then after the build finishes, I could simply cherry-pick files appropriate to a particular build setup.
I'm sure there is a better way, tho Coq doesn't make a lot of sense to be used as a bytecode [gets slow quick] , so indeed dune will try to use coqc native always to compile the stdlib, but we could tweak it.
As a Coq power user, I would certainly appreciate an official knob for dune to make the entire build native-only.
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:39):Note that the invariant is that even if after lib_root is used, always Coq is added to the package; the thing is that opam for example needs this lib_root, otherwise will place under lib/foo and that's to be avoided, I think Dune now provides a bit better ways to handle that.
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:41):So the use of lib_root is just a hack to install things in lib/coq, even for libraries where lib would be lib/foo
Aleksey Arens (Feb 12 2021 at 03:41):Does location /usr/pkg/lib/ocaml/site-lib/coq/theories/Arith/Arith.v look reasonable to you?
Aleksey Arens (Feb 12 2021 at 03:41):Emilio Jesús Gallego Arias said:
Note that the invariant is that even if after
lib_rootis used, always Coq is added to the package; the thing is that opam for example needs this lib_root, otherwise will place underlib/fooand that's to be avoided, I think Dune now provides a bit better ways to handle that.
Ok. Thank you for sharing this.
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:42):As a Coq power user, I would certainly appreciate an official knob for dune to make the entire build native-only.
That's the default, tho we build coqtop.byte and coqc.byte as a convenience, but that's easy to disable if it bothers you. I think tho that Dune will install libraries in both byte and native so save very little [unless wanna modify the lib files and tweak (mode ...)]
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:42):Does location /usr/pkg/lib/ocaml/site-lib/coq/theories/Arith/Arith.v look reasonable to you?
Looks good to me, if that's where pluginsis also installed
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:43):Ok. Thank you for sharing this.
yeah, it is confusing, I should document this, or improve the setup
Emilio Jesús Gallego Arias (Feb 12 2021 at 03:43):Hopefully soon each Coq package will go into its own directory so the hack will be compat only
Aleksey Arens (Feb 12 2021 at 03:44):Emilio Jesús Gallego Arias said:
Ok. Thank you for sharing this.
yeah, it is confusing, I should document this, or improve the setup
I would appreciate if the notes on the generation of .install files appear in INSTALL.md (or txt) or README.md (or txt) as applicable.
Aleksey Arens (Feb 12 2021 at 03:45):Emilio Jesús Gallego Arias said:
Hopefully soon each Coq package will go into its own directory so the hack will be compat only
As far as packaging goes, as long as I could with confidence make a decision on which files belong to package and have a correct locations, and which don't, there should be not much of an issue in practical packaging activities.
Aleksey Arens (Feb 12 2021 at 03:47):Emilio Jesús Gallego Arias said:
As a Coq power user, I would certainly appreciate an official knob for dune to make the entire build native-only.
That's the default, tho we build
coqtop.byteandcoqc.byteas a convenience, but that's easy to disable if it bothers you. I think tho that Dune will install libraries in both byte and native so save very little [unless wanna modify the lib files and tweak(mode ...)]
Would you say that a binary-only build of coq is a plausible state? I have never really used it w/o the bytecode set of packages. Do those play a particular role (I would guess ocamldebug usage is relevant there).
Aleksey Arens (Feb 12 2021 at 03:48):Also, concerning binary naming convention. Should coqc always correspond to a binary version, or it is possible for it to refer to a byte-code one as well under certain circumstances? I also assume that coqc.byte always refers to a byte-code version, and that is a newly adopted convention; please correct me if I'm wrong here.
Aleksey Arens (Feb 12 2021 at 03:50):Emilio Jesús Gallego Arias said:
Hi Aleksey Arens , excuse my unfamiliarity with pkgsrc; what is a PLIST file, what is the mismatch you see?
The PLIST is just a package file manifest. Check out example for coq at https://github.com/NetBSD/pkgsrc/blob/trunk/lang/coq/PLIST
Aleksey Arens (Feb 12 2021 at 06:01):I wonder, if someone have access to a working list of files inside a packages Coq 8.13.0. I would like to use for reference in my packaging effort. I have come across some discrepancies between the list of files present in the previous version, and the list of files generated by dune in the coq.install file.
Guillaume Melquiond (Feb 12 2021 at 07:37):Could you be more precise about those discrepancies? I just looked at the coq.install file you posted and it looks fine. As Emilio explained, as long as you have $lib == $lib_root/coq, it is correct. Ugly but correct.
Aleksey Arens (Feb 12 2021 at 07:51):Guillaume Melquiond said:
Could you be more precise about those discrepancies? I just looked at the
coq.installfile you posted and it looks fine. As Emilio explained, as long as you have$lib == $lib_root/coq, it is correct. Ugly but correct.
The lib_root and lib items had installed in the correct place in staging, so it's not an issue anymore.
I wonder if the .cmt / .cmti / .a files are needed in a package? Would something break for a developer using coq if I remove those files from a package?
Also, is the appearance of those
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__G_btauto.cmi" {"plugins/btauto/btauto_plugin__G_btauto.cmi"}
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__G_btauto.cmt" {"plugins/btauto/btauto_plugin__G_btauto.cmt"}
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__G_btauto.cmx" {"plugins/btauto/btauto_plugin__G_btauto.cmx"}
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__Refl_btauto.cmi" {"plugins/btauto/btauto_plugin__Refl_btauto.cmi"}
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__Refl_btauto.cmt" {"plugins/btauto/btauto_plugin__Refl_btauto.cmt"}
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__Refl_btauto.cmti" {"plugins/btauto/btauto_plugin__Refl_btauto.cmti"}
"_build/install/default/lib/coq/plugins/btauto/btauto_plugin__Refl_btauto.cmx" {"plugins/btauto/btauto_plugin__Refl_btauto.cmx"}
a result of new naming convention, associated with a slightly adjusted interpretation of .mlpack definitions? I have had hard time finding the description of how that name translation occurs; I assume it's within dune internals.
Some of the names that are missing from the 8.12.2 are
coq/plugins/btauto/refl_btauto.cmi
coq/plugins/btauto/refl_btauto.cmx
coq/plugins/btauto/g_btauto.cmx
coq/plugins/btauto/btauto_plugin.o
Are the .o files needed anymore? I do not see them in the list of files for 8.13.0.
Aleksey Arens (Feb 12 2021 at 08:00):What happened to the .pack directory convention? I'm seeing the following (basically, the .pack was present in the old version of the package).
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib.cmxa'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Gramext.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Gramext.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Grammar.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Grammar.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Plexing.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Plexing.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Ploc.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/gramlib/.pack/gramlib__Ploc.cmx'
Has something changed?
Guillaume Melquiond (Feb 12 2021 at 08:02):If I am not mistaken, the .o and .a were never needed; they are a compilation artifact. The .cmi files are needed when compiling a plugin. (I doubt anyone would ever need the .cmi files for plugins themselves, but who knows?) The .cmt and .cmti files are optional; they are useful for plugin developers who use Merlin during development, but not mandatory.
Guillaume Melquiond (Feb 12 2021 at 08:04):I think the .pack directories are also compilation artifacts. They should not have been installed.
Aleksey Arens (Feb 12 2021 at 08:04):Also, what about those:
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith.o'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith_base.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith_base.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Arith_base.o'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Between.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Between.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Between.o'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Bool_nat.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Bool_nat.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Bool_nat.o'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Compare.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Compare.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Compare.o'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Compare_dec.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Compare_dec.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Compare_dec.o'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Div2.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Div2.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/theories/Arith/.coq-native/NCoq_Arith_Div2.o'
I don't see NCoq_Arith_Div2 files in the .install anywhere. I do see coq/theories/Arith.v and coq/theories/Arith.vo.
Aleksey Arens (Feb 12 2021 at 08:05):I noticed that the .vos files are no longer present in the tree.
Guillaume Melquiond (Feb 12 2021 at 08:07):.vos and .vok files are useless when proper .vo files are installed.
Guillaume Melquiond (Feb 12 2021 at 08:07):As for .coq-native directories, it depends. If -native-compiler yes is passed at configuration time, they need to be installed. Otherwise not.
Aleksey Arens (Feb 12 2021 at 08:08):Guillaume Melquiond said:
If I am not mistaken, the
.oand.awere never needed; they are a compilation artifact. The.cmifiles are needed when compiling a plugin. (I doubt anyone would ever need the.cmifiles for plugins themselves, but who knows?) The.cmtand.cmtifiles are optional; they are useful for plugin developers who use Merlin during development, but not mandatory.
Thank you for sharing this. I'll get rid of .o and .a files then. Strangely, but .o were present in the previous PLIST. The .cmi have been useful in development since old times, so they are definitely to be kept. Good to know about .cmt and .cmti. I'm a user of Merlin myself, but has not quite had time to go through all of its details of operation thoroughly. Will be keeping those files as well then.
Aleksey Arens (Feb 12 2021 at 08:08):Guillaume Melquiond said:
.vosand.vokfiles are useless when proper.vofiles are installed.
Thank you for noting this. The old PLIST did actually have the .vos in addition to .vo.
Aleksey Arens (Feb 12 2021 at 08:09):Guillaume Melquiond said:
As for
.coq-nativedirectories, it depends. If-native-compiler yesis passed at configuration time, they need to be installed. Otherwise not.
The issue is that those directories are missing after a dune build. I definitely had a native compiler available.
Guillaume Melquiond (Feb 12 2021 at 08:10):The name is misleading. It means that the native_compute tactic is enabled. This is controlled during the invocation of the configure script.
Aleksey Arens (Feb 12 2021 at 08:11):Guillaume Melquiond said:
The name is misleading. It means that the
native_computetactic is enabled. This is controlled during the invocation of theconfigurescript.
Could you please go into more details thereby. Also, what knob should one turn to enable this with dune?
Guillaume Melquiond (Feb 12 2021 at 08:14):No idea; I am not even sure this is supported by dune. As for native_compute, it is a tactic that calls the ocamlopt compiler on the fly to hasten computations. There are three modes: yes, ondemand, and no. As the name implies, -native-compiler no disables the native_compute tactic. With -native-compiler yes, the standard library is precompiled, so that ocamlopt has less work to do on the fly. The default setting is -native-compiler ondemand, that is, the tactic is enabled, but nothing is precompiled. Precompiled files go into the .coq-native directories.
Aleksey Arens (Feb 12 2021 at 08:15):Guillaume Melquiond said:
No idea; I am not even sure this is supported by dune. As for
native_compute, it is a tactic that calls theocamloptcompiler on the fly to hasten computations. There are three modes:yes,ondemand, andno. As the name implies,-native-compiler nodisables thenative_computetactic. With-native-compiler yes, the standard library is precompiled, so thatocamlopthas less work to do on the fly. The default setting is-native-compiler ondemand, that is, the tactic is enabled, but nothing is precompiled. Precompiled files go into the.coq-nativedirectories.
So, if I do not include .coq-native directories, no functionality will be lost, apart perhaps from increase in compilation times in some cases?
Guillaume Melquiond (Feb 12 2021 at 08:16):Only if -native-compiler yes was not passed. Otherwise, Coq will try to find the precompiled files and complain loudly if it cannot find them.
Aleksey Arens (Feb 12 2021 at 08:18):I assume that dune had enable the native compilation, since there are .cmx files everywhere.
Aleksey Arens (Feb 12 2021 at 08:18):What about the name translation issue with plugin mentioned above?
Guillaume Melquiond (Feb 12 2021 at 08:19):Again, do not mistake the native compilation of Coq, with the precompilation of its standard library. Those are completely separate things.
Aleksey Arens (Feb 12 2021 at 08:20):Are .glob files necessary?
Guillaume Melquiond (Feb 12 2021 at 08:21):I don't think so.
Aleksey Arens (Feb 12 2021 at 08:21):Ok, thank you for clarification. You mentioned that it is "precompilation". Is there a way to actually compile the standard library after installation somehow?
Aleksey Arens (Feb 12 2021 at 08:21):Ok, thank you. I'm curious, what were they responsible for?
Guillaume Melquiond (Feb 12 2021 at 08:23):Regarding the change of plugin structures, this is specific to dune. This seems fine (but I am no dune user.)
Guillaume Melquiond (Feb 12 2021 at 08:24):.glob files are used during the creation of the documentation for hyperlinks. Once the documentation is done, they no longer have any use, but perhaps some other tools out there make use of them.
Guillaume Melquiond (Feb 12 2021 at 08:25):No, precompilation for native_compute happens at the exact same time .vo files are generated. There are plans to do it in two stages, but that is for a later release.
Aleksey Arens (Feb 12 2021 at 08:25):What about those:
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/topbin/coqc_bin.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/topbin/coqproofworker_bin.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/topbin/coqqueryworker_bin.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/topbin/coqtacticworker_bin.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/topbin/coqtop_bin.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/declareDef.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/declareDef.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/declareObl.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/declareObl.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/lemmas.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/lemmas.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/obligations.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/obligations.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/pfedit.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/pfedit.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/proof_global.cmi'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/lib/coq/vernac/proof_global.cmx'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/share/coq/coq-ssreflect.lang'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/share/coq/coq.lang'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/share/coq/coq.png'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/share/coq/coq_style.xml'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/share/coq/default.bindings'
pkg_create: can't stat `/usr/obj/pkgsrc/lang/coq/work/.destdir/usr/pkg/share/texmf-dist/tex/latex/coq/coqdoc.sty'
The lib ones are presumably moved/renamed files. I am a bit more surprised by the share ones.
Aleksey Arens (Feb 12 2021 at 08:28):FYI:
/usr/obj/pkgsrc/lang/coq/work/coq-8.13.0 %]
find . -iname '*.png'
./ide/coqide/coq.png
./doc/sphinx/_static/diffs-show-proof.png
./doc/sphinx/_static/diffs-coqide-multigoal.png
./doc/sphinx/_static/coqide.png
./doc/sphinx/_static/diffs-coqide-removed.png
./doc/sphinx/_static/diffs-error-message.png
./doc/sphinx/_static/diffs-coqide-on.png
./doc/sphinx/_static/diffs-coqtop-on.png
./doc/sphinx/_static/diffs-coqide-compacted.png
./doc/sphinx/_static/diffs-coqtop-on3.png
./doc/sphinx/_static/diffs-coqtop-compacted.png
./doc/sphinx/_static/coqide-queries.png
./doc/sphinx/_static/diffs-coqtop-multigoal.png
./dev/doc/shield-icon.png
I guess, the .png really belongs to coqide.
Aleksey Arens (Feb 12 2021 at 08:31):I'm not sure what coq_style.xml corresponds to. Nothing corresponding to default.bindings in sight as well.
Also,
/usr/obj/pkgsrc/lang/coq/work/coq-8.13.0 %]
find . -iname '*sty'
./_build/install/default/lib/coq/tools/coqdoc/coqdoc.sty
./_build/default/tools/coqdoc/coqdoc.sty
./doc/sphinx/_static/coqnotations.sty
./doc/sphinx/refman-preamble.sty
./tools/coqdoc/coqdoc.sty
Also, it seems that coq.lang and coq-ssreflect.lang really belong to the coqide, since they're currently under the ./ide directory.
Théo Zimmermann (Feb 12 2021 at 08:34):FYI native_compute is not enabled in the Dune build.
Théo Zimmermann (Feb 12 2021 at 08:35):It should become enabled soon in the master branch but not in 8.13.
Théo Zimmermann (Feb 12 2021 at 08:35):specific support needed to be added to Dune for this and it was only introduced in the very recent Dune 2.8
Aleksey Arens (Feb 12 2021 at 08:42):Ok. Thank you. I wonder, if the default build still operates in ondemand mode (as presented in table under the -native-compiler option here)?
And if it doesn't, can I enable ondemand mode when building with dune. (Since it really doesn't need to involve any build-manager acrobatics, conceptually speaking, it shouldn't be impossible.) If not, then perhaps, it could be achieved by a simple config change? Something that could fit into a small patch for 8.13 branch.
Aleksey Arens (Feb 12 2021 at 08:43):If it does, then essentially no functionality is lost, and 8.13.0 is good to go into production. If it does, however... that's a much harder question.
If it does, then perhaps I could help with back-porting to 8.13.0 when the feature appears in trunk.
Aleksey Arens (Feb 12 2021 at 08:47):Would you possibly recommend me a small coq script to test if native_compute works.
I have used Coq extensively myself, but have not really come across the need to use this feature; thus, I'm not entirely familiar with it.
Paolo Giarrusso (Feb 12 2021 at 08:48):@Aleksey Arens you want to (1) compile Coq itself to native code (as you’re doing), and (2) set “-native-compiler no” to disable compiling Coq .v files to native code, as dune does.
Paolo Giarrusso (Feb 12 2021 at 08:51):The story is longer, but the TLDR is that today native-compiler ondemand is a net negative (make Coq slower, a bit or a lot, for extremely little advantage in extremely rare cases).
Paolo Giarrusso (Feb 12 2021 at 08:53):For completeness, native-compiler yes does have (very limited) valid use-cases; I’d say your package is likely to be ready even without it.
Guillaume Melquiond (Feb 12 2021 at 08:57):Paolo Giarrusso said:
native-compiler ondemand is a net negative
Stop spreading misinformation. ondemand has absolutely zero impact on performances (unless you use native_compute obviously).
Paolo Giarrusso (Feb 12 2021 at 08:58):@Guillaume Melquiond it’s the first time I hear that response, but there are benchmarks on Github on this point.
Guillaume Melquiond (Feb 12 2021 at 09:00):No, there are not. If you were arguing about -native-compiler yes, then yes. But -nativer-compiler ondemand is a no-op; it does not perform any extra computation with respect to -native-compiler no.
Paolo Giarrusso (Feb 12 2021 at 09:01):“Try to load the library” has a non-zero cost (not “absolutely zero”); see https://github.com/coq/coq/issues/11107#issuecomment-567040281
Guillaume Melquiond (Feb 12 2021 at 09:02):I am impressed. You were using 8.13 in November 2019? Nice!
Paolo Giarrusso (Feb 12 2021 at 09:02):@Guillaume Melquiond of course not.
Guillaume Melquiond (Feb 12 2021 at 09:03):Then, do not take your 8.10 benchmark as meaning anything for Coq 8.13!
Paolo Giarrusso (Feb 12 2021 at 09:03):That sounds like “moving goalposts”. If that issue were now fixed, I’d be happy.
Aleksey Arens (Feb 12 2021 at 09:04):Is there absolutely no way to convert a theory to native code after the coq system is installed?
Aleksey Arens (Feb 12 2021 at 09:07):Should I keep .ml and .mli files in the tree? I guess, they help with ocamldebug. Are they usefull at all with Coq?
Guillaume Melquiond (Feb 12 2021 at 09:12):.ml and .mli files are only useful for Merlin users (or similar) who wants to "jump to location".
Aleksey Arens (Feb 12 2021 at 09:13):Ok. I guess, I'll keep them then...
Guillaume Melquiond (Feb 12 2021 at 09:13):Aleksey Arens said:
Is there absolutely no way to convert a theory to native code after the coq system is installed?
No, the .coq-native directory is filled by the call to coqc that creates the .vo corresponding file.
Aleksey Arens (Feb 12 2021 at 09:14):I do not quite follow you. When is the directory filled? I presume, at compile time.
Aleksey Arens (Feb 12 2021 at 09:14):What creates the .vo file? Corresponding to what? I see that .coq-native is populated by multiple files.
Guillaume Melquiond (Feb 12 2021 at 09:15):Yes, when you do coqc foo.v, it creates both foo.vo and .coq-native/foo.cmxs.
Aleksey Arens (Feb 12 2021 at 09:16):Aah. Ok. :neutral: :expressionless: :speechless: :speechless:
Aleksey Arens (Feb 12 2021 at 09:17):How soon are changes to dune build process coming? I assume, they would not be hard to backport.
Guillaume Melquiond (Feb 12 2021 at 09:23):Are you speaking in general? Or are you waiting for specific fixes?
Aleksey Arens (Feb 12 2021 at 09:26):I'm interested in ability to use native_compute, basically.
I think, the package could still make it into pkgsrc-current w/o native_compute, though.
Aleksey Arens (Feb 12 2021 at 09:29):Hm... i think current coq could be moved to lang/coq812, and the 8.13.0 could be packaged as lang/coq proper. So, there's no specific desirable time-frame.
Guillaume Melquiond (Feb 12 2021 at 09:30):With -native-compiler ondemand, you can use native_compute. But since files are not precompiled, it means you are paying a few extra seconds whenever you native_compute. But if the point is to replace a vm_compute that is taking several minutes, then even in ondemand mode, native_compute is still worth it.
Aleksey Arens (Feb 12 2021 at 09:33):Well, I would assume that one would be using native_compute for some large proof. So it makes sense to do it in a JIT fashion.
Aleksey Arens (Feb 12 2021 at 09:35):Is there a good way to enable the native_compute in ondemand mode in the source at this time, even with dune build defaulting to no?
Aleksey Arens (Feb 12 2021 at 09:35):If there is, then I could just give the user an option to build it with this option enabled, and keep it off by default.
Théo Zimmermann (Feb 12 2021 at 09:43):Yes. I think so. You just have to manually call ./configure yourself instead of letting Dune do it.
Théo Zimmermann (Feb 12 2021 at 09:44):Dune currently calls configure with -no-ask -native-compiler no -bin-annot.
Aleksey Arens (Feb 12 2021 at 09:44):Why not let dune do it? It actually already does this.
Aleksey Arens (Feb 12 2021 at 09:45):Exactly!
Aleksey Arens (Feb 12 2021 at 09:45):So, why not change -native-compiler no to -native-compiler yes?
Aleksey Arens (Feb 12 2021 at 09:45):ERR
Théo Zimmermann (Feb 12 2021 at 09:45):I'm answering your question regarding the possibility of enabling native_compute in ondemand mode.
Aleksey Arens (Feb 12 2021 at 09:45):Really meant to -native-compiler ondemand.
Théo Zimmermann (Feb 12 2021 at 09:46):You can edit your own messages. I'm not quite following what you're asking now.
Aleksey Arens (Feb 12 2021 at 09:47):I was asking if I run ./configure with -native-compiler ondemand from under dune (by e.g. editing dune file under config/dune ), would I be able to expect a correct build with dune?
Pierre Roux (Feb 12 2021 at 09:47):Paolo Giarrusso said:
That sounds like “moving goalposts”. If that issue were now fixed, I’d be happy.
You actively participated in the discussion, that's why we were expecting you to know that your problem is fixed in 8.13.
Théo Zimmermann (Feb 12 2021 at 09:47):Guillaume Melquiond said:
Aleksey Arens said:
Is there absolutely no way to convert a theory to native code after the coq system is installed?
No, the
.coq-nativedirectory is filled by the call tocoqcthat creates the.vocorresponding file.
Also, the quote above is not entirely correct as of today. @Pierre-Marie Pédrot has developed an external tool that allows producing the .coq-native output after the fact.
Aleksey Arens (Feb 12 2021 at 09:48):Théo Zimmermann said:
Guillaume Melquiond said:
Aleksey Arens said:
Is there absolutely no way to convert a theory to native code after the coq system is installed?
No, the
.coq-nativedirectory is filled by the call tocoqcthat creates the.vocorresponding file.Also, the quote above is not entirely correct as of today. Pierre-Marie Pédrot has developed an external tool that allows producing the
.coq-nativeoutput after the fact.
AHA!!! That really changes things a lot!
Aleksey Arens (Feb 12 2021 at 09:48):External == not in coq source tree, right?
Théo Zimmermann (Feb 12 2021 at 09:48):Aleksey Arens said:
I was asking if I run
./configurewith-native-compiler ondemandfrom under dune (by e.g. editing dune file under config/dune ), would I be able to expect a correct build with dune?
I think so, yes. I don't see what could go wrong. But maybe I'm mistaken. I'm not an expert in this part of the system/
Théo Zimmermann (Feb 12 2021 at 09:48):Aleksey Arens said:
External == not in coq source tree, right?
Right.
Aleksey Arens (Feb 12 2021 at 09:48):If so, then we got a solution. Disable -native-compiler in the system package as a matter of a general policy.
Guillaume Melquiond (Feb 12 2021 at 09:48):Aleksey Arens said:
External == not in coq source tree, right?
Yes, that is why I said it would be for a later release of Coq.
Aleksey Arens (Feb 12 2021 at 09:49):I'll just need to package one more package for pkgsrc, and that's it!
Théo Zimmermann (Feb 12 2021 at 09:49):Note that it's not yet a properly "released" package.
Aleksey Arens (Feb 12 2021 at 09:49):Guillaume Melquiond said:
Aleksey Arens said:
External == not in coq source tree, right?
Yes, that is why I said it would be for a later release of Coq.
I'm not sure what picture you have in mind her. Would the tool be available in the later release of Coq?
Théo Zimmermann (Feb 12 2021 at 09:49):But sure, you can go ahead and package it.
Théo Zimmermann (Feb 12 2021 at 09:50):Aleksey Arens said:
Guillaume Melquiond said:
Aleksey Arens said:
External == not in coq source tree, right?
Yes, that is why I said it would be for a later release of Coq.
I'm not sure what picture you have in mind her. Would the tool be available in the later release of Coq?
Yes, that's the plan eventually. Although, if it will be available in 8.14 or not is yet TBD.
Aleksey Arens (Feb 12 2021 at 09:50):Yes, working on it. Lots of manual adjustments to PLIST. So far "-coqide -doc" build looks functional.
Guillaume Melquiond (Feb 12 2021 at 09:50):If you use -native-compiler no, then native_compute is definitely disabled. You really need -native-compiler ondemand, even if you fill .coq-native after the fact.
Aleksey Arens (Feb 12 2021 at 09:50):But, is the tool working now? For someone who really needs it right now?
Théo Zimmermann (Feb 12 2021 at 09:51):Aleksey Arens said:
But, is the tool working now? For someone who really needs it right now?
I've never actually used it, but according to @Pierre-Marie Pédrot yes.
Aleksey Arens (Feb 12 2021 at 09:51):Ok then. That appears to be all I need to move forth. I'll attempt a build with ondemand later, either today, or tomorrow.
Aleksey Arens (Feb 12 2021 at 09:52):I wonder, if you may suggest me a good test script for testing native_compute functionality (looks like a custom tactics).
Aleksey Arens (Feb 12 2021 at 09:54):Actually, while we're at it. Is there a good tests targets already implemented in dune?
Aleksey Arens (Feb 12 2021 at 09:54):Something that I could run after package is built?
Théo Zimmermann (Feb 12 2021 at 09:54):Coq has a test-suite.
Théo Zimmermann (Feb 12 2021 at 09:55):But I don't know if it's any good for testing native_compute.
Pierre-Marie Pédrot (Feb 12 2021 at 09:58):That tool can be found in this PR: https://github.com/coq/coq/pull/13287
Pierre-Marie Pédrot (Feb 12 2021 at 09:59):It's part of the Coq repo, so the easiest way to get it is to compile a local version of Coq with the same OCaml variant as your target
Aleksey Arens (Feb 12 2021 at 10:11):Ok. I'll test those options (ondemand and the tool). Thank you.
Aleksey Arens (Feb 12 2021 at 10:13):Is there a script you might recommend me to test the native_compute functionality? Build success is, quite obviously, not a reliable indicator of working functionality.
Aleksey Arens (Feb 12 2021 at 12:21):Looking at the fileset, I noticed that Zify is available as a standalone plugin in the new build, while in the source tree it' under micromega directory. Why is Zify exposed as lib/coq/plugins/zify/zify_plugin.*?
Aleksey Arens (Feb 12 2021 at 12:23):I also don't see the csdpcert under the micromega in the .install file. The only mention of csdpcert is _build/install/default/bin/csdpcert.
Aleksey Arens (Feb 12 2021 at 14:51):Ok. Finished the audit of PLIST. Things look good right now. Will finalize things with doc and coqide build options tomorrow. Also, will try to check out the ondemand switch at that time.
Thank you all for your help. I really appreciate your time and expertise.
Aleksey Arens (Feb 12 2021 at 14:54):I assume the answer is "affirmative", but going to ask just in case: Do all of those belong to the final distribution?
lib/coq/tools/TimeFileMaker.py
lib/coq/tools/make-both-single-timing-files.py
lib/coq/tools/make-both-time-files.py
lib/coq/tools/make-one-time-file.py
I also assume likewise for this one:
lib/coq/tools/CoqMakefile.in
Please correct me if I'm wrong.
Théo Zimmermann (Feb 12 2021 at 15:01):Yes.
Emilio Jesús Gallego Arias (Feb 12 2021 at 15:58):@Aleksey Arens many of the changes you see are due to actually files being refactored, so they are fine; regarding the contents of the .install file, I think all that is there has to be installed if you want a full Coq setup, including the glob files as to correctly build plugins' docs etc...
Regarding the byte suffix, yes you can rely on it [it comes from a long convention in OCaml land], enabling -native yes with Dune and 8.13 is possible, but you need Dune 2.8 , to call configure manually, and to patch theories/dune and user-contrib/Ltac2/dune and dune-project [one line each]. Calling configure manually is required anyways in most packaging scenarios as to correctly set prefix.
Emilio Jesús Gallego Arias (Feb 12 2021 at 15:59):Why is Zify exposed as lib/coq/plugins/zify/zify_plugin.*
Because OCaml's -I option works at the level of directories, so you cannot have enough granularity otherwise
Théo Zimmermann (Feb 12 2021 at 17:24):You mean -native-compiler yes.
Emilio Jesús Gallego Arias (Feb 12 2021 at 19:38):Indeed, I was writing "pseudo code" XD
Aleksey Arens (Feb 13 2021 at 01:07):What releases do you think should be tracked for NetBSD? For me, the most relevant ones are the latest working release versions. Is trunk relevant for any use cases? I've never actually had to do it, but I could imagine a developer could benefit from such setup.
Aleksey Arens (Feb 13 2021 at 01:10):I've got dune 2.8. I'll be testing the native build soon.
Aleksey Arens (Feb 13 2021 at 01:20):So, what flavours do you think are most pertinent? Let's suppose the following structure:
coq-release for 8.13.X (options could control whether to use a branch build or a release tag)
coq-alpha for 8.14.X (options could control whether to use a branch build or a release tag)
coq-trunk
I'm mostly interested in coq-release for day-to-day use, and that matches not only my experience. Do you think there are reasonable community use cases for coq-alpha and coq-trunk?
I realize that building from trunk on an OS is in general a challenge, and there's a merit in a package like coq-trunk for this reason.
Guillaume Melquiond (Feb 13 2021 at 08:31):Honestly, I do not see the point of coq-alpha and coq-trunk. Coq users have never shown any interest in such packages. In fact, given the lack of feedback our beta packages usually get, we have even decided to not make any for the next release.
Enrico Tassi (Feb 13 2021 at 09:04):Today we build coq "trunk" using opam or nix, so if you want to ease this task on your favorite OS you should focus on these two tools.
Emilio Jesús Gallego Arias (Feb 13 2021 at 18:05):Coq's master branch could be indeed interesting to some, but the large majority of users will want to use latest stable versions of Coq + libraries [Coq platform]
Paolo Giarrusso (Feb 13 2021 at 22:52):@Aleksey Arens is the assumption that users upgrade when NetBSD pushes a new package, or are they allowed (and supported) if they hold back?
Paolo Giarrusso (Feb 13 2021 at 22:55):Also, is it to possible to install additional (coq) packages on top? Today they're mostly packaged using opam and maybe Nix.
Aleksey Arens (Feb 18 2021 at 09:46):Paolo Giarrusso said:
Also, is it to possible to install additional (coq) packages on top? Today they're mostly packaged using opam and maybe Nix.
What setup do you have in mind? I would be more than happy to consider various packaging schemes. Would you like to work out the setup perhaps? What do you think about an IRC session this weekend?
Aleksey Arens (Feb 18 2021 at 09:50):Enrico Tassi said:
Today we build coq "trunk" using opam or nix, so if you want to ease this task on your favorite OS you should focus on these two tools.
Thank you for sharing this feedback. I think, using opam on NetBSD to install OCaml packages works quite well. As long as opam (+ build system, e.g. dune) has the capability to install into a staging directory, and as long as the build system uses a sound autoconfiguration setup (which dune makes a really great attempt it already), I see no obstacles to a really seamless builds on NetBSD.
I guess, packaging-wise, I've got to update several older packages, and that's it. The build tools themselves (dune) and the packaging tools (opam) are already doing a great job (aside from relatively minor tweaks needed here and there, perhaps).
Aleksey Arens (Feb 18 2021 at 09:56):Guillaume Melquiond said:
Honestly, I do not see the point of
coq-alphaandcoq-trunk. Coq users have never shown any interest in such packages. In fact, given the lack of feedback our beta packages usually get, we have even decided to not make any for the next release.
Thank you. That is good to know. I myself have actually been using these packages, but usually through opam pin, and also by creating custom local packages for pkgsrc.
Emilio Jesús Gallego Arias said:
Coq's master branch could be indeed interesting to some, but the large majority of users will want to use latest stable versions of Coq + libraries [Coq platform]
I guess, I'll put coq-trunk into the wip repository for the few specifically interested. (The packages in wip do not need to be consistently buildable.)
Aleksey Arens (Feb 18 2021 at 09:58):Paolo Giarrusso said:
Aleksey Arens is the assumption that users upgrade when NetBSD pushes a new package, or are they allowed (and supported) if they hold back?
The users need to upgrade in general. Of course, with binary packages, this is not an absolute requirement, but in practice, the chain of dependencies is usually such that the upgrade is necessary anyway, especially given that the dependencies are built against newer release of source build instructions.
I wonder, if there's a particular good use case for Coq to stay at older versions? I would argue that there's a case for a coq-release package in general, but not sure whether older ones should be available seamlessly. Your feedback is welcome.
Aleksey Arens (Feb 18 2021 at 10:02):Paolo Giarrusso said:
Also, is it to possible to install additional (coq) packages on top? Today they're mostly packaged using opam and maybe Nix.
How do you imagine the case for accommodating various versions? Something along pkgviews perhaps (cf. 'symlink-based package management' / 'depot')? If yes, then it's something that I myself might have an interest in, though doubtful that pkgsrc would be able to accommodate this.
If we come to the case for porting e.g. Nix to NetBSD, then this could be a genuinely interesting project by all means. Let's talk.
Guillaume Melquiond (Feb 18 2021 at 10:16):Aleksey Arens said:
How do you imagine the case for accommodating various versions?
As a matter of fact, just changing a few lines on Coq's side would be sufficient to handle it, e.g., instead of having user-contrib/Foo, have user-contrib/Foo-1 and user-contrib/Foo-2. The difficult part (for any system you can think of) is: How do you inform of dependencies? In other words, who is responsible for telling that Foo-1 should be used in place of Foo-2 in a given situation?
Guillaume Melquiond (Feb 18 2021 at 10:22):To be more precise, it takes only a few lines of code to add an option coqtop -P Foo-1 that causes Foo-1 to be mapped in place of Foo-2. But is that how users want to manage versions?
Enrico Tassi (Feb 18 2021 at 10:28):Also, we have no notion of what other languages would call ABI, any dependency is super strict and imposed by the tips you require. Multiple versions is IMO not implementable today in any sane way.
Guillaume Melquiond (Feb 18 2021 at 10:37):Yes, that is why I am suggesting option -P Foo-1 as a portable shortcut for the already available option -Q /path/to/user-contrib/Foo-1 Foo. Anything more complicated is just infeasible with Coq.
Michael Soegtrop (Feb 18 2021 at 11:23):Please note that Coq Platform took a different approach for package variant paths (like CompCert for different architectures). I have a sibling folder to the coq library folder and put these there.
Michael Soegtrop (Feb 18 2021 at 11:24):See also (https://github.com/coq/coq/issues/12686)
Aleksey Arens (Feb 18 2021 at 15:59):Enrico Tassi said:
Also, we have no notion of what other languages would call ABI, any dependency is super strict and imposed by the tips you require. Multiple versions is IMO not implementable today in any sane way.
That's fine. I think the approach should in either case involve storing multiple versions of a package on a system.
Aleksey Arens (Feb 18 2021 at 16:02):Guillaume Melquiond said:
Aleksey Arens said:
How do you imagine the case for accommodating various versions?
As a matter of fact, just changing a few lines on Coq's side would be sufficient to handle it, e.g., instead of having
user-contrib/Foo, haveuser-contrib/Foo-1anduser-contrib/Foo-2. The difficult part (for any system you can think of) is: How do you inform of dependencies? In other words, who is responsible for telling thatFoo-1should be used in place ofFoo-2in a given situation?
Well, the binary is still unchanged. I doubt it's a good approach to switch library names for the same binary. If we treat the package holistically, then we have a consequence that no part of a package could be reliably altered. Ergo, we need to manage multiple *installations* somehow, rather than loading multiple library versions.
Guillaume Melquiond (Feb 18 2021 at 16:10):I do not understand what you mean by unchanged binary. The .vo files are certainly different. This is no different from having both libmpfr.so.4 and libmpfr.so.6 being installed on your system, with some programs/libraries dynamically linking against one, while others link against the other one. For example, CompCert is linked against Flocq-3 while some other libraries will link against Flocq-4 (once it is out).
Aleksey Arens (Feb 18 2021 at 16:11):Guillaume Melquiond said:
I do not understand what you mean by unchanged binary.
I mean something along the lines of /pkgs/coq-8.13.0/bin/coqtop vs e.g. /pkg/coq-8.13.1/bin/coqtop
Aleksey Arens (Feb 18 2021 at 16:29):Guillaume Melquiond said:
[...] For example, CompCert is linked against Flocq-3 while some other libraries will link against Flocq-4 (once it is out).
What about the following approach: there's one directory (corresponding to a distinct package version) with CompCert linked against Flocq-3, and there's another directory (corresponding to a distinct package version) with CompCert linked against Flocq-4. Yes, there shall be two installations of CompCert thus. Different installation combos could be generated by producing pre-packaged versions with different combinations.
Guillaume Melquiond (Feb 18 2021 at 16:32):No, that is not what this is about. CompCert is dynamically linked against Flocq 3.x, while CoqInterval is dynamically linked against Flocq 4.x. So, as it stands, it is impossible to install both CompCert and CoqInterval at the same time, because it is currently impossible to have two versions of Flocq (since they ar eboth installed in coq/user-contrib/Flocq).
Aleksey Arens (Feb 18 2021 at 16:50):Guillaume Melquiond said:
No, that is not what this is about. CompCert is dynamically linked against Flocq 3.x, while CoqInterval is dynamically linked against Flocq 4.x. So, as it stands, it is impossible to install both CompCert and CoqInterval at the same time, because it is currently impossible to have two versions of Flocq (since they ar eboth installed in
coq/user-contrib/Flocq).
Are paths used by CompCert and CoqInterval relative? I know, with .so (basic shared libraries) files on Unix, it's possible to specify a relative path for their other .so dependencies. In this case, we might just proceed with a similar approach.
However, I think that a more preferred approach would be to link against distinct coq paths, e.g. coq-8.13.0/user-contrib/Flocq-3 and coq-8.13.1/user-contrib/Flocq-4. This does mean that the paths should not be hardcoded in CompCert ; is this the case for CompCert?
A question: what usage scenario are you looking for in here? What about possibly launching different versions of the setups in different VMs?
Guillaume Melquiond (Feb 18 2021 at 17:16):Aleksey Arens said:
A question: what usage scenario are you looking for in here? What about possibly launching different versions of the setups in different VMs?
Yes, it would work, but this is just painful. I do not want to have several installations and have to switch depending on which Coq development I am working on. (I currently do, and this is no fun.)
Aleksey Arens said:
However, I think that a more preferred approach would be to link against distinct coq paths, e.g.
coq-8.13.0/user-contrib/Flocq-3andcoq-8.13.1/user-contrib/Flocq-4. This does mean that the paths should not be hardcoded in CompCert ; is this the case for CompCert?
The logical paths are hardcoded, not the physical ones. That is why I was talking about -Q /path/to/user-contrib/Flocq-3 Flocq, since this is the option to control which physical path gets mapped to which logical path (and -P Flocq-3 would just be a shortcut for it). But this option has to be passed to Coq at some point.
Emilio Jesús Gallego Arias (Feb 18 2021 at 17:40):Coq adds all of user-contrib to scope anyways so you will find many problems. At least Dune will start installing libraries in $lib/$pkg instead of in the global prefix [which causes huge slowdowns in some cases] at some point, also vendored libraries will be mangled so they can coexist, tho we could also adopt a policy for versioning if OCaml / OPAM upstream do it. For now, the only workaround is to name your libs with the version à la flocq-3 flocq-4.
Paolo Giarrusso (Feb 19 2021 at 19:13):@Aleksey Arens FWIW, I suspect you’re the only NetBSD user here (?), so I’m not sure a NetBSD-only solution would help with the other problems.
Aleksey Arens (Feb 19 2021 at 19:14):Paolo Giarrusso said:
Aleksey Arens FWIW, I suspect you’re the only NetBSD user here (?), so I’m not sure a NetBSD-only solution would help with the other problems.
I've been talking in more general terms terms; general packaging on systems that use hierarchical filesystems with global root to store package contents.
Paolo Giarrusso (Feb 19 2021 at 19:15):On the “multiple version” scenario — I’m not sure if that’s a problem with Nix (but with Nix I have more basic problems), but it is with opam. The scenario is what Guillaume mentioned — package A depends on foo-V1 and B depends on foo-V2.
Paolo Giarrusso (Feb 19 2021 at 19:15):With opam, you create separate “opam switches”, one containing foo-V1 and one with foo-V2.
Paolo Giarrusso (Feb 19 2021 at 19:15):annoyingly, even foo-independent packages must be recompiled from scratch for each switch.
Aleksey Arens (Feb 19 2021 at 19:16):Paolo Giarrusso said:
On the “multiple version” scenario — I’m not sure if that’s a problem with Nix (but with Nix I have more basic problems), but it is with opam. The scenario is what Guillaume mentioned — package A depends on foo-V1 and B depends on foo-V2.
I would like to suggest that we work out what a most general workable (i.e. something that is not quite over-engineered, and that could be implemented) is going to look like.
Paolo Giarrusso (Feb 19 2021 at 19:16):and just for extra fun, this also comes up when porting package A from foo-V1 to foo-V2
Aleksey Arens (Feb 19 2021 at 19:17):Paolo Giarrusso said:
annoyingly, even foo-independent packages must be recompiled from scratch for each switch.
Recompilation itself is not necessarily a problem, considering the lack of ABI in coq, particularly. And in general terms of system management, those are not really a huge problem, considering the capabilities of "workstation" class hardware that is relatively accessible these days.
Paolo Giarrusso (Feb 19 2021 at 19:20):s/workstation/throttling Intel laptop/ :-) — and personally, I’m annoyed each time I must rebuild OCaml _and_ Coq for these reasons, even if it takes (dunno) ten minutes. Other people must rebuild bigger ecosystems.
Paolo Giarrusso (Feb 19 2021 at 19:21):but I shouldn’t speak to the annoyances of others :-)
Aleksey Arens (Feb 19 2021 at 19:21):As i understand it, Nix does not operate in virtual isolated trees environment. It operates within a global hierarchical filesystem. Thus, it must be distinguishing between different installations through the use of different naming conventions. This does require a little bit of support from packages. Specifically:
(a) With very few exceptionts (think ssl certificates, and even that point is aruable), absolute paths should not be encoded into the package binaries, libraries, or data files.
(b) Relative paths could be encoded (think about the -R linker flag) in package libraries, binaries, and data.
Packages should support destdir style installation.
Aleksey Arens (Feb 19 2021 at 19:24):Paolo Giarrusso said:
s/workstation/throttling Intel laptop/ :-) — and personally, I’m annoyed each time I must rebuild OCaml _and_ Coq for these reasons, even if it takes (dunno) ten minutes. Other people must rebuild bigger ecosystems.
In my understanding, the compilation time is the price of consistency.
And even doing rebuilds of Coq on an old quad-core phenom (with 32G of ram, though, which is an important factor for these jobs), yields rather decent build times. Building on more powerful hardware feels like a breeze (on e.g. Xeon W 2XXX / 3XXX).
Paolo Giarrusso (Feb 19 2021 at 19:25):Coq packages for Nix already exist :-).
Aleksey Arens (Feb 19 2021 at 19:27):Paolo Giarrusso said:
Coq packages for Nix already exist :-).
I'll need to do a much deeper examination of Nix to understand how it works. With this knowledge, I would be able to make an informed decision, on how to achieve the desired capabilities in a manner harmonious with other package managers — whether pkgsrc or not.
Paolo Giarrusso (Feb 19 2021 at 19:29):Agreed. I’m not sure if Nix fixes all the problems for Nix users, and I’ve failed to become one.
Aleksey Arens (Feb 19 2021 at 19:30):In terms of requirements, what are we looking at specifically?
I doubt that rebuilds could be avoided at all. Is it important for you not to rebuild? Could we drop this requirement?
Do we need to have different variants of package installations (think about a single instance of the whole dependency set; another helpful picture is the set of packages in an opam switch) to be present on the same system?
Can we have different installation sets running in different virtual machines, as opposed to residing on the same system? After all, VM-level virtualization is already used on e.g. Qubes to virtualize away graphical desktop from applications.
Last updated: Oct 03 2023 at 04:02 UTC