Bug#1000491: FTBFS with Why3 1.4.0
Source: frama-c
Version: 20201209+titanium-4.1
Severity: serious
Tags: ftbfs
Dear Maintainer,
Frama-c FTBFS with Why3 1.4.0:
> [...]
> File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
> 31 | let config = Why3.Whyconf.load_default_config_if_needed config in
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: Unbound value Why3.Whyconf.load_default_config_if_needed
> make[1]: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
> make[1]: *** Waiting for unfinished jobs....
> make[1]: Leaving directory '/<<PKGBUILDDIR>>'
> dh_auto_build: error: make -j4 returned exit code 2
> make: *** [debian/rules:45: binary-arch] Error 25
> dpkg-buildpackage: error: debian/rules binary-arch subprocess returned exit status 2
This may be fixed by the new upstream release v23 (Vanadium).
Cheers,
--
Stéphane
-- System Information:
Debian Release: bookworm/sid
APT prefers testing
APT policy: (990, 'testing'), (500, 'unstable'), (1, 'experimental')
Architecture: amd64 (x86_64)
Foreign Architectures: i386
Kernel: Linux 5.14.0-4-amd64 (SMP w/4 CPU threads)
Locale: LANG=fr_FR.UTF-8, LC_CTYPE=fr_FR.UTF-8 (charmap=UTF-8), LANGUAGE not set
Shell: /bin/sh linked to /usr/bin/dash
Init: systemd (via /run/systemd/system)
LSM: AppArmor: enabled
Reply to: