Open MSoegtropIMC opened 4 years ago
Indeed, if we could wind back time, flexlink -version
would be a good addition! It’s displayed at the top of flexlink -help
, though
Ah sorry - I overlooked it : FlexDLL version 0.37fdopen2
I uploaded the log to my AWS account - Github seems to have some hickups (https://msoegtrop-public.s3.eu-central-1.amazonaws.com/CoqIdeFlexlink.zip)
A Gist is the other way to link large log files
Thanks, I will try this next time. If the size is the issue, Github could at least give a proper error message. I got "Something went really wrong - please try again" (about 10x).
Would scripts to get you to this point help?
Gist doesn-t work for me either - I get a time out during the upload after a few minutes - upload to AWS takes 2 seconds.
Here is the output of flexlink with export FLEXLINKFLAGS="-show-exports -show-imports -explain"
:
(https://msoegtrop-public.s3.eu-central-1.amazonaws.com/CoqIdeFlexlink_explain.zip)
Here is one of the error messages I get:
/usr/lib/gcc/x86_64-w64-mingw32/9.2.0/../../../../x86_64-w64-mingw32/bin/ld: C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3\liblablgtk3_stubs.a(cairo_pango_stubs.o): in function `caml_pango_cairo_error_underline_path':
/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/build/lablgtk3.3.1.1/_build/default/src/cairo_pango_stubs.c:177: undefined reference to `pango_cairo_error_underline_path'
collect2: error: ld returned 1 exit status
** Fatal error: Error during linking
If you can post the scripts yes, I think it might!
I will post the scripts tomorrow (there is a Coq workshop today)
@dra27 : I pushed the build scripts here : (https://github.com/MSoegtropIMC/coq-platform/tree/windows-8.12.0)
You need the opam and windows folders (this is pretty much the complete repo).
In the windows folder, adjust the paths in test_coq_platform.bat
to your liking. Then run this batch file. It should setup a new cygwin in the folder you specified, install opam and compile coq and coqide via opam.
The script should end with:
#=== ERROR while compiling coqide.8.12+beta1 ==================================#
# context 2.0.7 | win32/x86_64 | ocaml-variants.4.07.1+mingw64c | file://C:/bin/cygwin_coq_platform_mingw/build/opam/
# path ~/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/build/coqide.8.12+beta1
# command C:\bin\cygwin_coq_platform_mingw\bin\make.exe -j15 coqide-opt
# exit-code 2
# env-file ~/.opam/log/coqide-71064-be72be.env
# output-file ~/.opam/log/coqide-71064-be72be.out
### output ###
# [...]
# /home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/build/lablgtk3.3.1.1/_build/default/src/cairo_pango_stubs.c:175: undefined reference to `pango_cairo_layout_path'
# /usr/lib/gcc/x86_64-w64-mingw32/9.2.0/../../../../x86_64-w64-mingw32/bin/ld: C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/lib/lablgtk3\liblablgtk3_stubs.a(cairo_pango_stubs.o): in function `caml_pango_cairo_error_underline_path':
# /home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/build/lablgtk3.3.1.1/_build/default/src/cairo_pango_stubs.c:177: undefined reference to `pango_cairo_error_underline_path'
# collect2: error: ld returned 1 exit status
# ** Fatal error: Error during linking
#
# File "caml_startup", line 1:
# Error: Error during linking
# make[1]: *** [Makefile.ide:108: bin/coqide.exe] Error 2
# make[1]: *** Waiting for unfinished jobs....
# make[1]: Leaving directory '/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/build/coqide.8.12+beta1'
# make: *** [Makefile.make:178: submake] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coqide 8.12+beta1
└─
┌─ The following changes have been performed
│ ∗ install cairo2 0.6.1
│ ∗ install conf-cairo 1
│ ∗ install conf-gnome-icon-theme3 0
│ ∗ install conf-gtk3 18
│ ∗ install conf-gtksourceview3 0+1
│ ∗ install conf-pkg-config 1.2
│ ∗ install dune 2.6.1
│ ∗ install dune-configurator 2.6.1
│ ∗ install dune-private-libs 2.6.1
│ ∗ install lablgtk3 3.1.1
│ ∗ install lablgtk3-sourceview3 3.1.1
└─
# Run eval $(opam env) to update the current shell environment
The former state can be restored with:
C:\bin\cygwin_coq_platform_mingw\usr\x86_64-w64-mingw32\sys-root\mingw\bin\opam.exe switch import "C:/bin/cygwin_coq_platform_mingw/home/Michael/.opam/ocaml-variants.4.07.1+mingw64c/.opam-switch/backup/state-20200707102548.export"
ERROR coq_platform_cygwin_setup.bat failed
P.S.: running the script will take about 5GB of disk space in the folders you specified.
Previous versions of coqide stopped working with lablgtk3.3.0.beta7 and later. This looks like the same issue.
Did you examine the differences between these version of lablgtk3? Perhaps it's not related to flexdll at all, but due to the changes inside lablgtk3.
@fdopen: I spent about half a day looking into what is going on and as far as I can tell there are linker errors on missing symbols which are there and the library order is fine. It might be that labgtk changed the link order - I can check this. But to me it looks like a bug in the link phase. If it is flexlink's or ld's fault I cannot say, but from the debug dumps flexlink produces I would more say it is flexlink's fault.
I am currently in the process of moving the Coq Windows build from our old shell scripts to opam. Doing so, I have an issue with linking CoqIDE with flexlink. I (or ocamlfind) specify one archive twice on the command line like this:
liblablgtk3_stubs needs symbols defined in lpangocairo-1.0 and the
nm
tool tells me that the symbols are there. Still I get an error that the symbols are undefined.I looked into this with SysInternals ProcMon and all involved tools (flexlink, mingw gcc and ld) read the archives in the order libpangocairo and then lablgtk3_stubs. Notably pangocairo-1.0 is not read a second time although it is specified twice. As far as I know at least ld does not use objects in an archive when they don't contain currently needed symbols, so in this order pangocairo-1.0 get's ignored.
Another interesting point is that the command line to gcc does not contain libpangocairo at all, although it does read it later - not sure what kind of magic this is (See line 9175 in the attached log).
I must admit I am not 100% sure what version of flexlink I have since it is supplied by opam and it doesn't seem to have an option to display this.
If this helps I can supply batch/shell scripts which install a fresh cygwin and bring you to the point of this error.
P.S.: I tried to attach the ProcMon log as txt or zip - it won't let me giving obscure errors. I will try again after creating the issue.