ultimate
ultimate copied to clipboard
ultimate-pa
Install Ultimate on Mac
I tried to configure the eclipse development environment on MAC, but the project failed to compile. One problem is: Lexer cannot be resolved as a type in the following code.
private Unit reflectiveParse(final String fileName) throws IOException { final BoogieSymbolFactory symFactory = new BoogieSymbolFactory(); final Lexer lexer = new Lexer(new FileInputStream(fileName)); lexer.setSymbolFactory(symFactory); final Parser parser = new Parser(lexer, symFactory, mServices); parser.setFileName(fileName); try { return (Unit) parser.parse().value; } catch (final Exception e) { mLogger.fatal("syntax error: ", e); throw new RuntimeException(e); }
Is there anyone who has tried to install Ultimate on mac, can help me with this？
I checked the pom.xml file and found lexer and parser files are generated automatically from the flex file. Do I need to install some tools for this?
Hi! Did you follow the setup instructions in our wiki and install the tools mentioned there? And if so, did you encounter problems with any of the steps?
Hi! Did you follow the setup instructions in our wiki and install the tools mentioned there? And if so, did you encounter problems with any of the steps?
Hi, yes, I followed the wiki instructions. Now the only issue is some Lexer.java and Parser.java files cannot be generated successfully, which leads to the errors in 4 or 5 packages
- Which projects are affected? I.e., which projects are missing the lexer and parser files?
- If you do a clean rebuild of one such project (and only that one), does Eclipse give you some useful console output that could point to the problem?
For example, compiling the package: AutomataScriptParser, I got the following:
Buildfile: /ultimate/trunk/source/AutomataScriptParser/src/de/uni_freiburg/informatik/ultimate/plugins/source/automatascriptparser/build-parser.xml
BUILD FAILED java.lang.UnsupportedOperationException: The Security Manager is deprecated and will be removed in a future release at java.base/java.lang.System.setSecurityManager(System.java:425) at org.eclipse.ant.internal.core.ant.InternalAntRunner.run(InternalAntRunner.java:700) at org.eclipse.ant.internal.core.ant.InternalAntRunner.run(InternalAntRunner.java:532) at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:104) at java.base/java.lang.reflect.Method.invoke(Method.java:578) at org.eclipse.ant.core.AntRunner.run(AntRunner.java:374) at org.eclipse.ant.internal.launching.launchConfigurations.AntLaunchDelegate.runInSameVM(AntLaunchDelegate.java:291) at org.eclipse.ant.internal.launching.launchConfigurations.AntLaunchDelegate.launch(AntLaunchDelegate.java:253) at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:807) at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:718) at org.eclipse.debug.internal.core.LaunchConfiguration.launch(LaunchConfiguration.java:713) at org.eclipse.core.externaltools.internal.model.ExternalToolBuilder.launchBuild(ExternalToolBuilder.java:183) at org.eclipse.core.externaltools.internal.model.ExternalToolBuilder.doBuildBasedOnScope(ExternalToolBuilder.java:171) at org.eclipse.core.externaltools.internal.model.ExternalToolBuilder.build(ExternalToolBuilder.java:90) at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:832) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:220) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:263) at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:316) at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:45) at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:319) at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:371) at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:392) at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:154) at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:244) at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Total time: 105 milliseconds
It's hard to debug these things remotely. But from that message, the Java version could be an issue? We currently only support building Ultimate on JDK 11 to JDK 14; newer versions change some of the security concepts in Java.
It's hard to debug these things remotely. But from that message, the Java version could be an issue? We currently only support building Ultimate on JDK 11 to JDK 14; newer versions change some of the security concepts in Java.
Thanks a lot. I found another issue with the Mac platform. When a variable is defined with "var", the eclipse reported an error and asked to change to Java 10 for compilation.
I found another issue with the Mac platform. When a variable is defined with "var", the eclipse reported an error and asked to change to Java 10 for compilation.
I doubt this is Mac-related. It sounds like Eclipse is targeting some older Java version. You can try the following:
- Right-click on some project in the package explorer
- Go to
Properties > Java Compiler > Configure Workspace Settings - Make sure
Compiler Compliance Levelis set to 11.
I found another issue with the Mac platform. When a variable is defined with "var", the eclipse reported an error and asked to change to Java 10 for compilation.
I doubt this is Mac-related. It sounds like Eclipse is targeting some older Java version. You can try the following:
- Right-click on some project in the package explorer
- Go to
Properties > Java Compiler > Configure Workspace Settings- Make sure
Compiler Compliance Levelis set to 11.
Thanks, could you please send me the link of jdk 11 that you downloaded to make sure I use the same package with you.
Moreover, I found the file MANIFEST.MF in ACSLParser, it has one line: .... Bundle-RequiredExecutionEnvironment: JavaSE-1.8 ....
So my eclispe loads javaSE-1.8 instead of JAVASE-1.1. I don't know why two packages use two different jre library
Ah. OK, I use oracle jdk. is it different from openjdk?
In general, I don't think it should make a difference. But who knows... Specifically, the error about the var keyword is quite certainly unrelated.
Ah. OK, I use oracle jdk. is it different from openjdk?
In general, I don't think it should make a difference. But who knows... Specifically, the error about the
varkeyword is quite certainly unrelated.
Thanks a lot. I managed to fix this issue.
But I encountered other problems. In some projects, in the file MANIFEST.MF
(1) when it has: "Import-Package: com.sun.xml.bind.v2;version="2.2.0"" , an error is reported: No available bundle exports package 'com.sun.xml.bind.v2'
(2) when it has: "Require-Bundle: de.uni_freiburg.informatik.ultimate.lib.core, org.jdom", an error is reported : Bundle 'org.jdom' cannot be resolved
What problems could be?
I tried to download the jar package for com.sun.xml.bind.v2 and imported it to the project, it solved the problem. I don't think it's the best way.
I fixed all the compilation errors.
Still one problem when I try to run Automizer.
The error is the following:
java.lang.NullPointerException
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.loadControllerPlugin(PluginFactory.java:290)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.loadControllerPlugin(PluginFactory.java:251)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.
what problems could be?
Can you give us some information to reproduce this? How did you run Automizer, on which input, etc. ?
Can you give us some information to reproduce this? How did you run Automizer, on which input, etc. ?
I cannot start the developer GUI in Eclipse. I opened Debug-E4.product, clicked "Synchronize", and then "launched an Eclipse application", then the errors jumped out.
I have configured the path in the run configuration.
I copied the full error message below:
java.lang.NullPointerException
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.loadControllerPlugin(PluginFactory.java:290)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.loadControllerPlugin(PluginFactory.java:251)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.
org.osgi.framework.BundleException: Error starting module. osgi.identity; osgi.identity="org.eclipse.ui.workbench"; type="osgi.bundle"; version:Version="3.120.0.v20200829-1411"; singleton:="true" [id=156]
at org.eclipse.osgi.container.Module.doStart(Module.java:614)
at org.eclipse.osgi.container.Module.start(Module.java:468)
at org.eclipse.osgi.framework.util.SecureAction.start(SecureAction.java:506)
at org.eclipse.osgi.internal.hooks.EclipseLazyStarter.postFindLocalClass(EclipseLazyStarter.java:117)
at org.eclipse.osgi.internal.loader.classpath.ClasspathManager.findLocalClass(ClasspathManager.java:572)
at org.eclipse.osgi.internal.loader.ModuleClassLoader.findLocalClass(ModuleClassLoader.java:346)
at org.eclipse.osgi.internal.loader.BundleLoader.findLocalClass(BundleLoader.java:398)
at org.eclipse.osgi.internal.loader.sources.SingleSourcePackage.loadClass(SingleSourcePackage.java:41)
at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:473)
at org.eclipse.osgi.internal.loader.ModuleClassLoader.loadClass(ModuleClassLoader.java:171)
at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:521)
at java.base/java.lang.Class.getDeclaredConstructors0(Native Method)
at java.base/java.lang.Class.privateGetDeclaredConstructors(Class.java:3137)
at java.base/java.lang.Class.getConstructor0(Class.java:3342)
at java.base/java.lang.Class.getDeclaredConstructor(Class.java:2553)
at org.eclipse.core.internal.registry.osgi.RegistryStrategyOSGI.createExecutableExtension(RegistryStrategyOSGI.java:204)
at org.eclipse.core.internal.registry.ExtensionRegistry.createExecutableExtension(ExtensionRegistry.java:923)
at org.eclipse.core.internal.registry.ConfigurationElement.createExecutableExtension(ConfigurationElement.java:246)
at org.eclipse.core.internal.registry.ConfigurationElementHandle.createExecutableExtension(ConfigurationElementHandle.java:63)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.createInstance(PluginFactory.java:304)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.loadControllerPlugin(PluginFactory.java:286)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.loadControllerPlugin(PluginFactory.java:251)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginFactory.
I solve the application problem. Everything works well now. Thanks a lot for your help.
I give a hint here. When trying to start the eclipse graphic UI in macOS, the plug-in: org.eclipse.swt.cocoa.macosx.x86_64 should be selected.
@maul-esel One request. Now the eclipse graphic UI version works very well. I try to install a command line version. I built the project by using "makeFresh.sh". The build is successful, but it seems makeFresh.sh is only written for linux instead of Mac. So I got the following message at the end of the building:
Using Taipan (taipan) as toolname Building .zip for linux... Version is 7ea82506 No termination toolchain specified, ommitting... No LTL toolchain specified, ommitting... No termination witness validation toolchain specified, ommitting... Removing old UTaipan-linux Copying files readlink: illegal option -- e usage: readlink [-fn] [file ...] adds/LICENSE* does not exist, aborting... bash makeZip.sh Taipan linux AutomizerCInline_WitnessPrinter.xml NONE AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml NONE NONE failed with bash
I believe it is a problem with macOS. Could you give some hints to modify makeFresh.sh to adopt it to macOS.
Great to hear that you got it to build :tada:
Regarding makeFresh.sh: I'm not very familiar with this script, so the following is somewhat based on guesses.
- You can try replacing
readlink -feinmakeZip.shby onlyreadlink -f, if the relevant files all exist it should (?) not make a difference. - @Heizmann has been trying to make the Mac build work, maybe he can help more here. As I see it, you probably have to add your platform to the platforms in line 15 of
makeFresh.sh, and apparently one has to add the platform totarget-platform-configurationintrunk/source/BA_MavenParentUltimate/pom.xml, though I am unsure of the concrete values to enter.
Great to hear that you got it to build 🎉
Regarding
makeFresh.sh: I'm not very familiar with this script, so the following is somewhat based on guesses.
- You can try replacing
readlink -feinmakeZip.shby onlyreadlink -f, if the relevant files all exist it should (?) not make a difference.- @Heizmann has been trying to make the Mac build work, maybe he can help more here. As I see it, you probably have to add your platform to the platforms in line 15 of
makeFresh.sh, and apparently one has to add the platform totarget-platform-configurationintrunk/source/BA_MavenParentUltimate/pom.xml, though I am unsure of the concrete values to enter.
Thanks, I tried to modify the these files and rebuild a mac version. But still got the following error. Please help to have a look when you are available:
[INFO] --- tycho-p2-repository-plugin:1.7.0:assemble-repository (default-assemble-repository) @ UltimateRepository --- [INFO] {osgi.os=macosx, osgi.ws=cocoa, org.eclipse.update.install.features=true, osgi.arch=x86_64} [ERROR] Cannot resolve project dependencies: [ERROR] Software being installed: Debug-E4 0.2.2 [ERROR] Missing requirement: Debug-E4 0.2.2 requires 'org.eclipse.equinox.p2.iu; BA_FeatureUltimateDebug.feature.group [0.2.2,0.2.3)' but it could not be found [ERROR] [ERROR] See http://wiki.eclipse.org/Tycho/Dependency_Resolution_Troubleshooting for help.
Hi @ShlKan, your latest issue has recently been solved in the merged pull request #630. Note that the script for a full release build is currently not prepared to support macOS. As soon as I have time, I will integrate the macOS build into the release script. Nevertheless, you should now be able to build Ultimate from scratch according to the instructions mentioned in pull request #630.
