Stream: Coq users

Topic: dune build / fileset / netbsd


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 12 2021 at 03:16):

exception, we could tweak it, but other packages must still install there

view this post on Zulip Emilio Jesús Gallego Arias (Feb 12 2021 at 03:16):

Also you have some space to tweak depending how do you call configure

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Feb 12 2021 at 03:19):

that's easy to tweak tho / patch if you want

view this post on Zulip 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

view this post on Zulip 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, not lib/foo as 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 12 2021 at 03:39):

Oh, no file should go under lib , all files go under lib/coq

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Aleksey Arens (Feb 12 2021 at 03:41):

Emilio Jesús Gallego Arias said:

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.

Ok. Thank you for sharing this.

view this post on Zulip 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 ...)]

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.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 ...)]

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.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.

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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 08:04):

I think the .pack directories are also compilation artifacts. They should not have been installed.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:05):

I noticed that the .vos files are no longer present in the tree.

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 08:07):

.vos and .vok files are useless when proper .vo files are installed.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:08):

Guillaume Melquiond said:

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.

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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:08):

Guillaume Melquiond said:

.vos and .vok files are useless when proper .vo files are installed.

Thank you for noting this. The old PLIST did actually have the .vos in addition to .vo.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:09):

Guillaume Melquiond said:

As for .coq-native directories, it depends. If -native-compiler yes is 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.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:11):

Guillaume Melquiond said:

The name is misleading. It means that the native_compute tactic is enabled. This is controlled during the invocation of the configure script.

Could you please go into more details thereby. Also, what knob should one turn to enable this with dune?

view this post on Zulip 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.

view this post on Zulip 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 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.

So, if I do not include .coq-native directories, no functionality will be lost, apart perhaps from increase in compilation times in some cases?

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:18):

I assume that dune had enable the native compilation, since there are .cmx files everywhere.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:18):

What about the name translation issue with plugin mentioned above?

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:20):

Are .glob files necessary?

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 08:21):

I don't think so.

view this post on Zulip 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?

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:21):

Ok, thank you. I'm curious, what were they responsible for?

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 08:26):

The lib ones are presumably moved/renamed files. I am a bit more surprised by the share ones.

view this post on Zulip 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

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:29):

I guess, the .png really belongs to coqide.

view this post on Zulip 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

view this post on Zulip Aleksey Arens (Feb 12 2021 at 08:33):

Also, it seems that coq.lang and coq-ssreflect.lang really belong to the coqide, since they're currently under the ./ide directory.

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 08:34):

FYI native_compute is not enabled in the Dune build.

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 08:35):

It should become enabled soon in the master branch but not in 8.13.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 09:02):

I am impressed. You were using 8.13 in November 2019? Nice!

view this post on Zulip Paolo Giarrusso (Feb 12 2021 at 09:02):

@Guillaume Melquiond of course not.

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 09:03):

Then, do not take your 8.10 benchmark as meaning anything for Coq 8.13!

view this post on Zulip Paolo Giarrusso (Feb 12 2021 at 09:03):

That sounds like “moving goalposts”. If that issue were now fixed, I’d be happy.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:13):

Ok. I guess, I'll keep them then...

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:14):

I do not quite follow you. When is the directory filled? I presume, at compile time.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:16):

Aah. Ok. :neutral: :expressionless: :speechless: :speechless:

view this post on Zulip 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.

view this post on Zulip Guillaume Melquiond (Feb 12 2021 at 09:23):

Are you speaking in general? Or are you waiting for specific fixes?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:44):

Dune currently calls configure with -no-ask -native-compiler no -bin-annot.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:44):

Why not let dune do it? It actually already does this.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:45):

Exactly!

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:45):

So, why not change -native-compiler no to -native-compiler yes?

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:45):

ERR

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:45):

I'm answering your question regarding the possibility of enabling native_compute in ondemand mode.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:45):

Really meant to -native-compiler ondemand.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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-native directory is filled by the call to coqc that creates the .vo corresponding 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.

view this post on Zulip 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-native directory is filled by the call to coqc that creates the .vo corresponding 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.

AHA!!! That really changes things a lot!

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:48):

External == not in coq source tree, right?

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:48):

Aleksey Arens said:

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?

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/

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:48):

Aleksey Arens said:

External == not in coq source tree, right?

Right.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:49):

I'll just need to package one more package for pkgsrc, and that's it!

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:49):

Note that it's not yet a properly "released" package.

view this post on Zulip 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?

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:49):

But sure, you can go ahead and package it.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:50):

But, is the tool working now? For someone who really needs it right now?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:54):

Actually, while we're at it. Is there a good tests targets already implemented in dune?

view this post on Zulip Aleksey Arens (Feb 12 2021 at 09:54):

Something that I could run after package is built?

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:54):

Coq has a test-suite.

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 09:55):

But I don't know if it's any good for testing native_compute.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Aleksey Arens (Feb 12 2021 at 10:11):

Ok. I'll test those options (ondemand and the tool). Thank you.

view this post on Zulip 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.

view this post on Zulip 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.*?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 15:01):

Yes.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Feb 12 2021 at 17:24):

You mean -native-compiler yes.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 12 2021 at 19:38):

Indeed, I was writing "pseudo code" XD

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 13 2021 at 01:10):

I've got dune 2.8. I'll be testing the native build soon.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Aleksey Arens (Feb 18 2021 at 09:56):

Guillaume Melquiond said:

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.

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Feb 18 2021 at 11:24):

See also (https://github.com/coq/coq/issues/12686)

view this post on Zulip 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.

view this post on Zulip 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, 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?

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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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-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?

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 19 2021 at 19:15):

With opam, you create separate “opam switches”, one containing foo-V1 and one with foo-V2.

view this post on Zulip Paolo Giarrusso (Feb 19 2021 at 19:15):

annoyingly, even foo-independent packages must be recompiled from scratch for each switch.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Feb 19 2021 at 19:21):

but I shouldn’t speak to the annoyances of others :-)

view this post on Zulip 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:

  1. (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.

  2. (b) Relative paths could be encoded (think about the -R linker flag) in package libraries, binaries, and data.

  3. Packages should support destdir style installation.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Feb 19 2021 at 19:25):

Coq packages for Nix already exist :-).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Aleksey Arens (Feb 19 2021 at 19:30):

In terms of requirements, what are we looking at specifically?

  1. I doubt that rebuilds could be avoided at all. Is it important for you not to rebuild? Could we drop this requirement?

  2. 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?

  3. 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: Jan 31 2023 at 14:03 UTC