Michael Soegtrop (Apr 03 2021 at 07:03): Michael Soegtrop (Apr 03 2021 at 07:03):This is a follow up on the Undefined symbols when loading printers discussion.
As it looks the -custom option has the effect that printers cannot be loaded into ocamldebug, both on Mac and Linux. On Linux -no-custom is default, so this didn't surface. On Mac -custom is default while -no-customactually works. As far as I understand this, this option only influences the bytecode build and not the native build. Furthermore the main point of the bytecode build is to be able to debug it. So is there any good reason to have the -custom default on Mac? Since this influences only bytecode, I guess the user risk of changing this would be marginal.
I wanted to add on the documentation of @Jason Gross a few words on how to use ocamldebug to analyze slow Qed - which is quite effective once one has the debugger running. But as a prerequisite I would like to have a working bytecode build at least on Mac and Linux in the platform.
@Emilio Jesús Gallego Arias mentioned that what works might also be influenced by the switch to dune, so we might want to wait with a decision until after that switch. Still I don't see a good reason to have -custom the default on Mac and -no-custom the default on Linux when on both only -no-custom works.
I plan to do a platform release early next week, and I think it might make sense to change it already for that.
Emilio Jesús Gallego Arias (Apr 03 2021 at 17:41):Actually I think dune build on mac doesn't use -custom, as indeed there is little reason to do so nowadays; likely -custom was added to mac for archaic reasons, we should check the git log [I did so in the past where we discussed about this with OCaml upstream but honestly I totally forgot]
Emilio Jesús Gallego Arias (Apr 03 2021 at 17:42):Our OCaml makefiles hadn't seen refresh in a long time, this is one of the advantages of using Dune, despite it being quite new, on the other hand they should handle for us quite a few of OCaml's idionsyncracies when cross-compiling or under different platforms.
Emilio Jesús Gallego Arias (Apr 03 2021 at 17:42):By the way we didn't try to cross compile Coq, but it should be possible !
Michael Soegtrop (Apr 03 2021 at 17:55):Emilio Jesús Gallego Arias said:
By the way we didn't try to cross compile Coq, but it should be possible !
I guess the issue will be to compile the standard library then. Afaik .vo files are not portable between systems and if one cross compiles say Windows Coq on Linux, one couldn't run the created Coq. Already under cygwin this is a tricky business cause of the different paths in cygwin and a MinGW app.
Emilio Jesús Gallego Arias (Apr 03 2021 at 17:57):Indeed that would be main difficulty to overcome, but IIANM Dune should provide support to actually run the target binaries.
Michael Soegtrop (Apr 03 2021 at 17:57):Regarding -no-custom I will then create a PR.
@Enrico Tassi : would you find it agreeable to change this in the upcomming Coq Platform - it could be easily done on opam level if it is too late to change the makefile. Or should we wait for 8.14 with this?
Michael Soegtrop (Apr 03 2021 at 17:57):Dune should provide support to actually run the target binaries.
How would this work? Wine?
Emilio Jesús Gallego Arias (Apr 03 2021 at 17:58):For master note that #13617 should have the same effect and we hope it lands soon, I think we should test this change in master first.
Michael Soegtrop (Apr 03 2021 at 17:58):Of cause mid term it would be nice to have portable .vo files - at least between all 32 a bit and all 64 bit platforms.
Michael Soegtrop (Apr 03 2021 at 18:00):Yes, it might be a bit hacky for the Coq Platform with Coq 8.13.2. I have some personal issues with this, but I know to get around this and I guess there are few others which have such issues.
Emilio Jesús Gallego Arias (Apr 03 2021 at 18:00):Actually indeed support for running binaries on the target context is missing, so indeed we would need to do some hack.
Emilio Jesús Gallego Arias (Apr 03 2021 at 18:01):But indeed seems like using wine would work at least for windows https://github.com/ocaml-cross/opam-cross-windows
Enrico Tassi (Apr 03 2021 at 18:35):Last time I tried cross compiling to windows with dune I lost one day and then fall back using dune on cygwin, that with the https://github.com/avsm/setup-ocaml action is trivial to set up in CI (and BTW is very close to what the platform scripts do).
Enrico Tassi (Apr 03 2021 at 18:36):@Michael Soegtrop I did not follow this discussion, what would we need to change for custom? the opam package?
Pierre-Marie Pédrot (Apr 03 2021 at 21:27):FTR, I was under the naive impression that vo files were not portable across architectures (i.e. 32 vs 64 bits) but they were portable across systems.
Pierre-Marie Pédrot (Apr 03 2021 at 21:27):If there are counterexamples to that, it would be 1. interesting to study and 2. probably worth a bug report.
Emilio Jesús Gallego Arias (Apr 04 2021 at 00:45):Actually good point @Pierre-Marie Pédrot , tho for us as we include the digest of plugins now too that would make them not portable, tho that's easy to disable with a flag. Cross compilation to win is supported and in active use in production AFAICT so if anyone would like to try I'll be happy to help with the dune + ocaml part.
Michael Soegtrop (Apr 04 2021 at 05:57):@Pierre-Marie Pédrot : if this is so, I think it would be due time to actually test it. It shouldn't be that difficult as a final step in platform CI.
Michael Soegtrop (Apr 04 2021 at 06:02):@Enrico Tassi : with -custom one cannot load the printers into ocamldebug, which partially defeats the purpose of a bytecode build. I know that there is also OCaml function tracing in a bytecode coqtop, but I usually make heavy use of the "time-machine" feature of ocamldebug when looking at the guts of Coq.
Enrico Tassi (Apr 04 2021 at 11:33):I was asking what needs to be done in order to not pass this option? I a patch to the opam package enough, or it is too invasive? I'm OK with the principle, but you ask me, and I'm afraid I don't know what I should/can do to help you (known next week I'm 90% off)
Michael Soegtrop (Apr 04 2021 at 14:32):I was asking what needs to be done in order to not pass this option?
It can be passed to configure in opam, so no need to patch the sources or makefiles.
Michael Soegtrop (Apr 04 2021 at 14:33):I mean either -custom or -no-custom can be passed to configure and on Mac -custom is the default.
Last updated: Sep 09 2024 at 06:02 UTC