Как настроить солвер Z3 на машине Travis-CI

Question

У меня есть проект с использованием библиотеки Z3 solver, и я хочу применить Travis-CI для непрерывного тестирования. Однако я не смог настроить z3 на удаленном компьютере в Travis-CI.

Вот дополнительная информация о моем проекте:

• Создано из IDE Eclipse Mars
• Используйте JDK 8
• Используйте Ant для сборки build.xml

Файл содержимого .travis.yml

 language: java
 sudo: enabled
 jdk:
   - oraclejdk8
 before_install:
 - sudo apt-get update
 - sudo apt-get install z3 -y
 script:
 - ant build
 - ant 'MyJUnitTest'

Вывод на удаленную консоль машины

... (be removed for clarity)
$ sudo apt-get install z3 -y
Reading package lists... Done
Building dependency tree       
Reading state information... Done
E: Unable to locate package z3
The command "sudo apt-get install z3 -y" failed and exited with 100 during .
Your build has been stopped.

Я понял, что проблему можно решить, добавив хранилище, содержащее решатель Z3, в .travis.yml (раздел before_install ). Я нашел один репозиторий: https://launchpad.net/~hvr/+archive/ubuntu/z3. Однако этот репозиторий больше не работает. Более ясно, что через 10 минут (время ожидания по умолчанию на компьютере с Travis-CI) ответ из этого хранилища не поступает.

$ sudo add-apt-repository ppa:hvr/z3

More info: https://launchpad.net/~hvr/+archive/ubuntu/z3
Press [ENTER] to continue or ctrl-c to cancel adding it
No output has been received in the last 10m0s, this potentially indicates a stalled build or something wrong with the build itself.
Check the details on how to adjust your build configuration on: https://docs.travis-ci.com/user/common-build-problems/#Build-times-out-because-no-output-was-received
The build has been terminated

Answer 1

Насколько я знаю, нет официального / поддерживаемого способа сделать это. Было бы неплохо, если бы действительно был репо. Но это можно сделать с помощью некоторого взлома, непосредственно выпуская выпуски и устанавливая их на сборочной машине.

Использование ночных сборок Z3

Люди Z3 поддерживают ночные сборки на github, поэтому действительно возможно получить последний код и интегрировать его с Travis-CI (для Linux и Mac), а также с Appveyor (для Windows).

В качестве примера того, как сделать это в travis, см .:

https://github.com/LeventErkok/sbv/blob/master/.travis.yml#L46-L66

Для настройки Appveyor см .:

https://github.com/LeventErkok/sbv/blob/master/.appveyor.yml#L10-L13

В зависимости от ваших конкретных потребностей, вы должны быть в состоянии принять это к вашей собственной проблеме. (Обратите внимание, что бит travis делает немного больше, чем z3, устанавливая некоторые другие зависимости на Mac; вы должны их пропустить. Ping, если вам нужна помощь!)

Примечание о стабильности

К сожалению, этот прием не на 100% защищен от ошибок и требует периодического обслуживания, поскольку зависит от того, где хранится Z3, как называются ночные сборки, как travis / appveyor обрабатывает среду и т. Д .; но это работало для меня довольно надежно в течение достаточно долгого времени. Удачи!

Использование стабильных версий Z3

Если вы хотите «стабильную» сборку вместо «ночной» z3, вы можете использовать аналогичный прием, слегка изменив локации; по сути, получая их от: https://github.com/Z3Prover/bin/tree/master/releases вместо https://github.com/Z3Prover/bin/tree/master/nightly