Frama-C Bug Tracking System - Frama-C
View Issue Details
0002223Frama-CKernel > Makefilepublic2016-04-11 13:592016-05-10 10:28
normaltexthave not tried
0002223: Frama-C upgrade installation not foolproof
I 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.
No tags attached.
log install.log (2,636) 2016-04-11 13:59
log install_122.log (15,008) 2016-04-28 17:34
Issue History
2016-04-11 13:59JochenNew Issue
2016-04-11 13:59JochenStatusnew => assigned
2016-04-11 13:59JochenAssigned To => signoles
2016-04-11 13:59JochenFile Added: install.log
2016-04-12 09:00signolesAssigned Tosignoles => virgile
2016-04-18 10:08maronezeNote Added: 0006179
2016-04-28 11:21JochenNote Added: 0006181
2016-04-28 17:34JochenFile Added: install_122.log
2016-04-28 17:39JochenNote Added: 0006182
2016-04-28 18:13maronezeNote Added: 0006183
2016-05-09 10:45JochenNote Added: 0006188
2016-05-10 08:29virgileNote Added: 0006189
2016-05-10 10:28JochenNote Added: 0006190

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.
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.
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.)
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.
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.)
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.
2016-05-10 10:28   
Ok, I see. If it's intended, I'm fine with it.