search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
52 stars 31 forks source link

mcrl2 compiling rewriter in compiled osx-clang version 3.0 #87

Closed jacopol closed 6 years ago

jacopol commented 7 years ago

lps2lts-sym abp.lps libc++abi.dylib: terminating with uncaught exception of type mcrl2::runtime_error: Could not load rewriter: rewriter version does not match the version of the calling application.

This applies to the compiled distribution version 3.0 for osx-clang.

This alternative works: lps2lts-sym --mcrl2-rewriter=jitty abp.lps

Note that the compiled rewriter can be much faster, but if it is impossible to get it compiled, using jitty should probably become the default option.

Meijuh commented 7 years ago

Ah yes, this is definitely a problem. The --jittyc compiler will not work unless you have precisely the same xcode version as Travis uses. OSX does not ship with a static libc++ so the only two options are:

  1. Do a binary release for every xcode version.
  2. Configure the binary release to use the jitty rewriter by default.

If you ask me the latter option seems more reasonable.

jacopol commented 7 years ago

Yes, let’s go for (non-compiling) jitty by default (but only for the binary distribution; is that possible?).

On 17 Aug 2017, at 15:24, Jeroen Meijer notifications@github.com<mailto:notifications@github.com> wrote:

Ah yes, this is definitely a problem. The --jittyc compiler will not work unless you have precisely the same xcode version as Travis uses. OSX does not ship with a static libc++ so the only two options are:

  1. Do a binary release for every xcode version.
  2. Configure the binary release to use the jitty rewriter by default.

If you ask me the latter option seems more reasonable.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/utwente-fmt/ltsmin/issues/87#issuecomment-323072378, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AGZgZdsUDA2Wi9ers9kabYE-EvVZFLqPks5sZD8LgaJpZM4M0UPp.

-- Prof. Jaco van de Pol University of Twente (NL) Formal Methods and Tools http://www.cs.utwente.nl/~vdpol

Meijuh commented 7 years ago

Yes that is definitely possible. I am wondering if we should only use jitty for OSX in the binary release (and not linux) or do we want consistent binary releases?

jacopol commented 7 years ago

I would say: Only for OSX. The default should be the compiling rewriter since it is usually faster, but we fall back on the interpreter in case the compiling rewriter is not available, like on OSX.

alaarman commented 7 years ago

This problem in OSX is often resolved by a compiler option -stdlib=libstdc++ or -stdlib=libc++

Meijuh commented 7 years ago

@alaarman could you maybe further explain why that would resolve the problem? Note that the lps2lts-sym binaries are already dynamically linked with libc++.