Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002223Frama-CKernel > Makefilepublic2016-04-11 13:592016-05-10 10:28
Assigned Tovirgile 
PrioritynormalSeveritytextReproducibilityhave not tried
PlatformSodium-20150201OSOS Version14.04.1-Ubuntu
Product Version 
Target VersionFixed in Version 
Summary0002223: Frama-C upgrade installation not foolproof
DescriptionI tried to follow the file "acslplusplus/frama-c/INSTALL" in order to upgrade Frama-C from version "Sodium-20150201" to the current version in the acslplusplus/frama git repository. The file "install.log" documents my attempts; lines starting with "sh> #" are comments I added subsequently to explain my motives; other lines starting with "sh>" are my command-line inputs; the rest is opam output.

As I've done everything in a newly cloned virtual machine, the state before the first and after the last command-line input is preserved, so if any particular information is needed, let me know, there is a good chance that I can provide it.
TagsNo tags attached.
Attached Fileslog file icon install.log [^] (2,636 bytes) 2016-04-11 13:59
log file icon install_122.log [^] (15,008 bytes) 2016-04-28 17:34

- Relationships

-  Notes
maroneze (developer)
2016-04-18 10:08

Thank you for the report.

Could you please tell us the version of OPAM that you are using? `opam --version` should output it.

Also, could you tell us if you have installed an external solver such as aspcud? Sometimes OPAM behaves quite erratically without such solvers.

I'll try to reproduce it locally, so I need to configure my OPAM accordingly.
Jochen (reporter)
2016-04-28 11:21

(Sorry for the delay; I was in holidays until yesterday.)

Opam reports version "1.2.1". Meanwhile, I've been told that I had better used a more mature version; so maybe this issue isn't worth the effort of fixing. I intend to try a newer version in a fresh virtual machine in the next days, and to report the results here.

As for external solvers, I don't know what that means, but neither the bash command "apropos aspcud" nor "locate aspcud" found something appropriate. Probably I don't have an external solver. Maybe a hint could be given in the Frama-C installation guide for Opam.
Jochen (reporter)
2016-04-28 17:39

I made another attempt, documented in file "install_122.log". Upgrading to opam 1.2.2 alone didn't help, but installing aspcud did, so maybe the role of external solvers should be more emphasized in the installation guide.

(I had still problems installing why3; if you have an idea how to fix them, please let me know.)
maroneze (developer)
2016-04-28 18:13

Thank you for the log file and the reports. I had already had a few issues due to the lack of aspcud, but your log file does confirm that they are indeed very nasty.

We already put some extra messages about aspcud in the upcoming Frama-C installation file, but we'll try to emphasize them even more.

From your log, it seems that your OPAM was somewhat broken before installing aspcud, and from then on it couldn't obtain a pristine state. There are some known issues with OPAM (hopefully to be fixed in the next release) that in some cases may prevent it from completely restoring a proper state without manual intervention (i.e. erasing some or most OPAM files and starting over).

I'm afraid the only sane solution would be to clean opam and restart from scratch, that is, erasing ~/.opam and doing a new `opam init`, then installing the packages again, this time with aspcud installed from the start.
Jochen (reporter)
2016-05-09 10:45

I followed your advice and could install frama-c magnesium without further problems - tnak you very much.

If you don't need my intermediate virtual machines (containing the states of failed installation attempts), I'd like to delete them.

(As a side remark, "frama-c -version" doesn't print a '\n' character at the end of its output line.)
virgile (developer)
2016-05-10 08:29

> (As a side remark, "frama-c -version" doesn't print a '\n' character at the end of its output line.)

This is intended, as frama-c -version is supposed to be used from scripts (e.g. ./configure of an external plugin). Scripts tend sometimes to have issues with a newline character (admittedly, frama-c could try to detect whether it is launched on a terminal or not and put a newline in the former case). frama-c -h will give you the version number in a more friendly way, though.
Jochen (reporter)
2016-05-10 10:28

Ok, I see. If it's intended, I'm fine with it.

- Issue History
Date Modified Username Field Change
2016-04-11 13:59 Jochen New Issue
2016-04-11 13:59 Jochen Status new => assigned
2016-04-11 13:59 Jochen Assigned To => signoles
2016-04-11 13:59 Jochen File Added: install.log
2016-04-12 09:00 signoles Assigned To signoles => virgile
2016-04-18 10:08 maroneze Note Added: 0006179
2016-04-28 11:21 Jochen Note Added: 0006181
2016-04-28 17:34 Jochen File Added: install_122.log
2016-04-28 17:39 Jochen Note Added: 0006182
2016-04-28 18:13 maroneze Note Added: 0006183
2016-05-09 10:45 Jochen Note Added: 0006188
2016-05-10 08:29 virgile Note Added: 0006189
2016-05-10 10:28 Jochen Note Added: 0006190

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker