Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Advice on running Frama-C Magnesium on Windows?

I had performed some experiments with Frama-C Sodium and Magnesium, 
using Cygwin+MinGW+WODI. I was able to compile and run Frama-C with its 
GUI, but I did not test most plugins. In particular, I did not test 
Alt-Ergo.

I just updated the Frama-C wiki with the steps I had to do:

https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:compiling_from_source

Please note that this is not officially supported.

As can be seen in the wiki, it's a somewhat lengthy process which 
requires several tweaks and is thus not very robust. I tried to identify 
and explain each issue I encountered along the way, but if you find and 
fix other problems, please do not hesitate to add them to the wiki.

I also performed some tests using OPAM for Windows (from Protzenko's 
website, which comes from Allsop's fork), which has not yet been 
officially released, however I did not manage to get lablgtk working via 
OPAM. I'll maybe try OCPWin next time.

Finally, as Loïc mentioned, currently it is probably faster to configure 
a Linux virtual machine and use it to compile and run Frama-C. The Linux 
release is also more stable, since it avoids Cygwin/Windows-specific issues.

Best regards,

On 02/01/2016 10:51 AM, John Eriksson wrote:
> I have been trying to compile Frama-C with GTK graphics and all in
> Cygwin for a couple of days now, but run into issues frequently. The
> compilation frequently fails as there appears to be a version mismatch
> between lablgtk2/gdk.cmi and ocaml (which is probably Cygwin's fault,
> I installed lablgtk and ocaml directly in Cygwin's setup manager so
> the versions should match). Some various other issues occur too
> (manual compilation of lablgtk fails due to varcc.cmo missing, etc.).
> Also, if I am not mistaken, Alt-Ergo is not included but must be
> compiled separately. This failed too as I needed Ocamlgraph, which in
> turn also failed due to the same gdk.cmi issue.
>
> The compilation instructions for Windows could use an update. Wodi has
> not been maintained for some time, and the latest Frama-C version that
> can be installed with it is Neon (it does work just fine though, with
> GUI and all relevant dependencies installed).
>
> Any advice on how to make it work (in Cygwin/Mingw/anything else), or
> would it be safer to just run a virtual machine with Linux?
>
> // John Eriksson
> KTH
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss

-- 
André Maroneze
Ingénieur-chercheur CEA/LIST
Laboratoire Sûreté et Sécurité des Logiciels