z3 4.8.7 #46991

nunoplopes · 2019-11-20T20:03:28Z

Created with brew bump-formula-pr.

nunoplopes · 2019-11-21T11:58:12Z

Not sure why Dafny started failing now. I don't think paths changed..

Bo98 · 2019-11-21T22:09:06Z

I think dafny might symlink z3 based on the Cellar location (which changes on version upgrades), which might be worth fixing to use the opt directory.

nunoplopes · 2019-11-21T22:44:16Z

Ah, thanks I see the problem. Dafny does:
(libexec/"z3/bin").install_symlink which("z3")

Which then points a specific version of Z3.
I don't know how to fix this in the way you describe. My thought was to create a bash script that simply forwards the arguments to z3. Would that be ok or did you have something else in mind?
Thanks!

chenrui333 · 2019-11-21T22:44:28Z

looks like duplicate of #46966

Bo98 · 2019-11-21T22:46:53Z

Would that be ok or did you have something else in mind?

I'd probably avoid using which altogether and use Formula["z3"].opt_bin/"z3".

Bo98 · 2019-11-21T23:00:54Z

I recommend also revision bumping dafny so that users will receive the update.

Bo98 · 2019-11-22T20:58:39Z

Ok that worked for everything except High Sierra:

[ERROR] FATAL UNHANDLED EXCEPTION: System.TypeInitializationException: The type initializer for 'System.Drawing.GDIPlus' threw an exception. ---> System.DllNotFoundException: libgdiplus.dylib assembly:<unknown assembly> type:<unknown type> member:(null)
  at (wrapper managed-to-native) System.Drawing.GDIPlus.GdiplusStartup(ulong&,System.Drawing.GdiplusStartupInput&,System.Drawing.GdiplusStartupOutput&)
  at System.Drawing.GDIPlus..cctor () [0x000b0] in <f1498bbfcd1c4b8797d09077fd282cd5>:0 
   --- End of inner exception stack trace ---
  at System.Drawing.Icon.Dispose () [0x00011] in <f1498bbfcd1c4b8797d09077fd282cd5>:0 
  at (wrapper remoting-invoke-with-check) System.Drawing.Icon.Dispose()
  at System.Drawing.Icon.Finalize () [0x00000] in <f1498bbfcd1c4b8797d09077fd282cd5>:0

Apologies for dragging you into dafny issues. If can maybe have a further look myself this weekend.

Bo98 · 2019-11-24T07:46:39Z

@BrewTestBot test this please

bayandin · 2019-11-24T23:15:49Z

Ok that worked for everything except High Sierra:

[ERROR] FATAL UNHANDLED EXCEPTION: System.TypeInitializationException: The type initializer for 'System.Drawing.GDIPlus' threw an exception. ---> System.DllNotFoundException: libgdiplus.dylib assembly:<unknown assembly> type:<unknown type> member:(null)
  at (wrapper managed-to-native) System.Drawing.GDIPlus.GdiplusStartup(ulong&,System.Drawing.GdiplusStartupInput&,System.Drawing.GdiplusStartupOutput&)
  at System.Drawing.GDIPlus..cctor () [0x000b0] in <f1498bbfcd1c4b8797d09077fd282cd5>:0 
   --- End of inner exception stack trace ---
  at System.Drawing.Icon.Dispose () [0x00011] in <f1498bbfcd1c4b8797d09077fd282cd5>:0 
  at (wrapper remoting-invoke-with-check) System.Drawing.Icon.Dispose()
  at System.Drawing.Icon.Finalize () [0x00000] in <f1498bbfcd1c4b8797d09077fd282cd5>:0

Apologies for dragging you into dafny issues. If can maybe have a further look myself this weekend.

For me, it helped to rebuild mono-libgdiplus and then install dafny.

Also, there is a release of boogie so we could switch resource to an archive:

   resource "boogie" do
-    url "https://github.com/boogie-org/boogie.git",
-      :revision => "9e74c3271f430adb958908400c6f6fce5b59000a"
+    url "https://github.com/boogie-org/boogie/archive/v2.4.1.tar.gz"
+    sha256 "af86ed63ab31c694aafa4912f7bf6f77ae3fce673d9f18d28c75cf7b95c0a1c6"
   end

Bo98 · 2019-11-24T23:18:19Z

That's interesting. I wonder what's broken about the current bottle of mono-libgdiplus. Ideally we'd want to avoid it happening again.

Could you, with the broken mono-libgdiplus, try add

ENV["MONO_LOG_LEVEL"] = "debug"
ENV["MONO_LOG_MASK"] = "dll"

to the dafny install script and see if that says why it won't load it?

bayandin · 2019-11-24T23:38:58Z

Hm, for me it looks like the original error message is misleading and formula mono-libgdiplus was not rebuilt (for High Sierra only?) after changes in dependency:

Mono: DllImport error loading library 'libgdiplus.dylib': 'dlopen(libgdiplus.dylib, 9): Library not loaded: /usr/local/opt/giflib/lib/libgif.7.dylib
  Referenced from: /usr/local/lib/libgdiplus.dylib
  Reason: Incompatible library version: libgdiplus.dylib requires version 8.0.0 or later, but libgif.7.dylib provides version 0.0.0'.
Mono: DllImport error loading library 'libgdiplus.dylib': 'dlopen(libgdiplus.dylib, 9): Library not loaded: /usr/local/opt/giflib/lib/libgif.7.dylib
  Referenced from: /usr/local/lib/libgdiplus.dylib
  Reason: Incompatible library version: libgdiplus.dylib requires version 8.0.0 or later, but libgif.7.dylib provides version 0.0.0'.
Mono: DllImport error loading library 'libgdiplus.dylib': 'dlopen(libgdiplus.dylib, 9): Library not loaded: /usr/local/opt/giflib/lib/libgif.7.dylib
  Referenced from: /usr/local/lib/libgdiplus.dylib
  Reason: Incompatible library version: libgdiplus.dylib requires version 8.0.0 or later, but libgif.7.dylib provides version 0.0.0'.
Mono: DllImport error loading library 'libgdiplus.dylib.so': 'dlopen(libgdiplus.dylib.so, 9): image not found'.
Mono: DllImport error loading library 'libgdiplus.dylib.bundle': 'dlopen(libgdiplus.dylib.bundle, 9): image not found'.
Mono: DllImport error loading library 'libgdiplus.dylib': 'dlopen(libgdiplus.dylib, 9): Library not loaded: /usr/local/opt/giflib/lib/libgif.7.dylib
  Referenced from: /usr/local/lib/libgdiplus.dylib
  Reason: Incompatible library version: libgdiplus.dylib requires version 8.0.0 or later, but libgif.7.dylib provides version 0.0.0'.
Mono: DllImport unable to load library 'dlopen(libgdiplus.dylib, 9): Library not loaded: /usr/local/opt/giflib/lib/libgif.7.dylib
  Referenced from: /usr/local/lib/libgdiplus.dylib
  Reason: Incompatible library version: libgdiplus.dylib requires version 8.0.0 or later, but libgif.7.dylib provides version 0.0.0'.

Here is the full log: dafny.log

Also, otool -L /usr/local/Cellar/mono-libgdiplus/6.0.4/lib/libgdiplus.dylib outputs for the current (broken) bottle:

	/usr/local/opt/mono-libgdiplus/lib/libgdiplus.0.dylib (compatibility version 1.0.0, current version 1.0.0)
->	/usr/local/opt/glib/lib/libglib-2.0.0.dylib (compatibility version 6201.0.0, current version 6201.1.0)
	/usr/local/opt/gettext/lib/libintl.8.dylib (compatibility version 10.0.0, current version 10.6.0)
	/usr/local/opt/cairo/lib/libcairo.2.dylib (compatibility version 11603.0.0, current version 11603.0.0)
	/usr/local/opt/freetype/lib/libfreetype.6.dylib (compatibility version 24.0.0, current version 24.1.0)
	/usr/local/opt/jpeg/lib/libjpeg.9.dylib (compatibility version 13.0.0, current version 13.0.0)
->	/usr/local/opt/libtiff/lib/libtiff.5.dylib (compatibility version 10.0.0, current version 10.0.0)
->	/usr/local/opt/giflib/lib/libgif.7.dylib (compatibility version 8.0.0, current version 8.0.0)
	/usr/local/opt/libpng/lib/libpng16.16.dylib (compatibility version 54.0.0, current version 54.0.0)
	/usr/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.11)
	/usr/local/opt/libexif/lib/libexif.12.dylib (compatibility version 16.0.0, current version 16.3.0)
	/usr/local/opt/fontconfig/lib/libfontconfig.1.dylib (compatibility version 14.0.0, current version 14.0.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.200.5)

and after rebuilding:

	/usr/local/opt/mono-libgdiplus/lib/libgdiplus.0.dylib (compatibility version 1.0.0, current version 1.0.0)
->	/usr/local/opt/glib/lib/libglib-2.0.0.dylib (compatibility version 6201.0.0, current version 6201.2.0)
	/usr/local/opt/gettext/lib/libintl.8.dylib (compatibility version 10.0.0, current version 10.6.0)
	/usr/local/opt/cairo/lib/libcairo.2.dylib (compatibility version 11603.0.0, current version 11603.0.0)
	/usr/local/opt/freetype/lib/libfreetype.6.dylib (compatibility version 24.0.0, current version 24.1.0)
	/usr/local/opt/jpeg/lib/libjpeg.9.dylib (compatibility version 13.0.0, current version 13.0.0)
->	/usr/local/opt/libtiff/lib/libtiff.5.dylib (compatibility version 11.0.0, current version 11.0.0)
->	/usr/local/opt/giflib/lib/libgif.dylib (compatibility version 0.0.0, current version 7.2.0)
	/usr/local/opt/libpng/lib/libpng16.16.dylib (compatibility version 54.0.0, current version 54.0.0)
	/usr/lib/libz.1.dylib (compatibility version 1.0.0, current version 1.2.11)
	/usr/local/opt/libexif/lib/libexif.12.dylib (compatibility version 16.0.0, current version 16.3.0)
	/usr/local/opt/fontconfig/lib/libfontconfig.1.dylib (compatibility version 14.0.0, current version 14.0.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.200.5)

Bo98 · 2019-11-24T23:49:28Z

Thank you!

The interesting thing is the Mojave has identical output but it seems to work there.

I'll get a revision bump sorted and check and see if there's any more that might need it.

Bo98 · 2019-11-25T00:02:44Z

#47141

Bo98 · 2019-11-25T19:17:09Z

mono-libgdiplus is fixed so let's retry this.

@BrewTestBot test this please

Bo98 · 2019-11-25T19:45:50Z

All good.

Thanks for your first pull request @nunoplopes! Merged now.

Apologies for the rocky road along the way!

z3 4.8.7

14c7b05

dafny: fix z3 symlink as suggested by Bo Anderson

98d51c1

dafny: bump revision number

eb20f5b

Bo98 mentioned this pull request Nov 23, 2019

python 3.8.0 #45337

Closed

10 tasks

Bo98 mentioned this pull request Nov 25, 2019

revision bumps for giflib #47141

Closed

antoniovs1029 mentioned this pull request Nov 25, 2019

Reenabling MacOS tests that had an issue with libgdiplus dotnet/machinelearning#4500

Merged

Bo98 closed this in c652503 Nov 25, 2019

nunoplopes deleted the z3-4.8.7 branch November 25, 2019 20:38

lock bot added the outdated PR was locked due to age label Jan 1, 2020

lock bot locked as resolved and limited conversation to collaborators Jan 1, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

z3 4.8.7 #46991

z3 4.8.7 #46991

nunoplopes commented Nov 20, 2019

nunoplopes commented Nov 21, 2019

Bo98 commented Nov 21, 2019

nunoplopes commented Nov 21, 2019

chenrui333 commented Nov 21, 2019

Bo98 commented Nov 21, 2019

Bo98 commented Nov 21, 2019

Bo98 commented Nov 22, 2019

Bo98 commented Nov 24, 2019

bayandin commented Nov 24, 2019

Bo98 commented Nov 24, 2019

bayandin commented Nov 24, 2019

Bo98 commented Nov 24, 2019

Bo98 commented Nov 25, 2019

Bo98 commented Nov 25, 2019

Bo98 commented Nov 25, 2019

z3 4.8.7 #46991

z3 4.8.7 #46991

Conversation

nunoplopes commented Nov 20, 2019

nunoplopes commented Nov 21, 2019

Bo98 commented Nov 21, 2019

nunoplopes commented Nov 21, 2019

chenrui333 commented Nov 21, 2019

Bo98 commented Nov 21, 2019

Bo98 commented Nov 21, 2019

Bo98 commented Nov 22, 2019

Bo98 commented Nov 24, 2019

bayandin commented Nov 24, 2019

Bo98 commented Nov 24, 2019

bayandin commented Nov 24, 2019

Bo98 commented Nov 24, 2019

Bo98 commented Nov 25, 2019

Bo98 commented Nov 25, 2019

Bo98 commented Nov 25, 2019