Наконец-то дошли руки попробовать компиляцию в нативный код (aka AOT compilation) от GraalVM.

Написал Hello World на java, выбрал GraalVM в качестве JVM, подключил официальный плагин Gradle, запустил nativeCompile и… все, оно скомплировалось и работает. Без ошибок, без разбора какой-то дичи, просто заработало сразу и все. Минут 15 на все про все ушло.

Ладно, попробуем что-нибудь поинтереснее — схавает ли GraalVM Spring с его рефлексией и прокси-классами в рантайме? Создаем простенький контроллер, теперь уже на Kotlin, который выплевывает JSON. Компилируем и… оно тоже работает! о_О

Я просто в шоке, до чего дошел прогресс. Ожидал веселых или не очень потрахушек примерно как с Kotlin native или с KotlinJS, но испытал преимущественно позитивные эмоции. Справедливости ради, на большом проекте все-таки магия сломалась:

Caused by: com.oracle.graal.pointsto.constraints.UnsupportedFeatureException: No instances of CensoredLoggerContext are allowed in the image heap as this class should be initialized at image runtime.

Возможно, еще вернусь к подобным экспериментам в будущем, интересно на перф-тесты всего этого посмотреть.

Единственная проблемка, которая возникла — нужно корректно выставлять JAVA_HOME при компиляции. Кроме этого отмечу, что компиляция довольно долгая (1 контроллер на спринге компилировался аж 2 минуты). Разумеется, больше получается конечный файл — 73 Мб (при этом fat jar занимает 22 Мб), но с учетом того, что сама JVM занимает больше 200 Мб, это фигня.

Опять появился рабочий мак, опять надо что-то делать с раскладкой. Гореть в аду тем, кто в левом нижнем углу размещает Fn вместо Ctrl! Другой прикол — поставить вместо ~ знак параграфа § — кто его вообще использует? Не помню, когда его в последний раз видел.

Тащить что-то тяжелое вроде karabiner, как в прошлый раз, не хотелось. Fn вместо Ctrl легко поменялись через обычные настройки клавиатуры, а вот для ~ пришлось немного баш-команд выполнить.

Надеюсь, ни для кого уже не секрет, что “приватный режим” в браузерах вообще ни разу не приватный. Комбинация заголовков, информации от JS и локации по IP-адресу и т.п. сама по себе может быть уникальна. Проверить свой браузер можно еще тут. Чуть сгладить проблему в Firefox можно с помощью настройки privacy.resistFingerprinting = true.

С одной стороны не очень весело, что приватность в интернете кончилась, с другой — киберпанк, который мы заслужили.

P.S. это все конечно прикольно на компе, но будет ли кто-то с этим морочиться на телефоне?:)

Постоянным читателям хорошо известно, что я недолюбливаю java. Как только я начал чуть забывать, почему, она решила мне преподнести очередной сюрприз. Возьмем простенький класс

public class TestClass {
  public void foo(){ System.out.println(getBar()); }

  String getBar(){ return "bar"; }
}

И создадим от него наследника, переопределяя метод (довольно частый прием в тестах):

new TestClass(){
  String getBar() { return "baz"; }
}.foo();

Как думаете, что выведет foo?

В процессе поиска ответов на свои вопросы про cvc5 наткнулся на конспект по солверам. Это большой сборник примеров. Очень легко читается (и он на рунглише), местами написана чушь, но он неплох для погружения в область, если кому интересна эта тема. От души разбавлено байками.

Среди интересного можно увидеть ломание генератора случайных чисел, решение задачки из комикса xkcd, доказательство корректности всяких битовых хаков, факторизацию числа, решение задачи расцветки графа, чтобы занимать меньше регистров памяти, поиск коллизий в CRC32, минимизацию количества тестов.

Когда-то я в качестве калькулятора использовал bc. Но потом мне открыли глаза на очевидную истину: лучший калькулятор для командной строки — это питон.

Только недавно я узнал (а может вспомнил, просто уже давно забыл), что в интерпретаторе можно использовать _ для использования предыдущего результата:

>>> 9 + 10
19
>>> _ * 12
228
>>>

По совету Петра Георгиевича после z3 решил попробовать солвер cvc5.

У него есть API, который почти полностью повторяет синтаксис z3 — надо просто заменить импорт на from cvc5.pythonic import * и убрать z3.. (Ну или в стиле злодеев сделать import cvc5.pythonic as z3). Однако данные из модели выковыриваются немного по-другому: вместо

model.eval(el).as_long()

надо писать

model[el].ast.getIntegerValue()

С получением результатов еще связан один очень дебильный баг (и это не только у меня руки кривые).

Несмотря на то, что cvc5 побеждает на конкурсах, на моей машине работал он ощутимо медленнее. Если z3 решил судоку за 100мс примерно (и это с учетом запуска интерпретатора), то cvc5 пыхтел аж 9,5 секунд. Решение для магического квадрата 5x5 он не нашел. А для рюкзака нет аналога Optimization из z3.

За разумное время последние две проблемы я решить не смог. Вообще cvc5 показался существенно менее дружелюбным к пользователю с точки зрения документации и настройки по сравнению с z3. С учетом ниши, которую я описывал ранее, z3 выглядит более адекватно.

Оказывается, в баше есть встроенная команда command, которая изначально предназначена для запуска исполняемого файла, имя которого совпадает со какой-нибудь встроенной командой баша. Однако command -v можно использовать для проверки, существует ли исполняемый файл в принципе.

Более очевидный способ — использовать which, который еще и путь покажет, но внезапно, это не самый лучший вариант:

• which может отсутствовать в некоторых системах (особенно если система урезана под контейнер);
• which на некоторых системах может не устанавливать код ошибки;
• which может вызывать под капотом пакетный менеджер.

Чтобы отредактировать и выполнить длинную команду-колбасу с помощью редактора, можно воспользоваться Ctrl+X+E. Мне это пригодилось для длинных curl.

В редакторе может не быть включен мягкий перенос строк, тогда пользы будет немного. В nano это решается Esc+$ или добавлением set softwrap в ~/.nanorc.

Солвер — это инструмент, который позволяет задать систему неравенств и прочих условий, и на выходе дать решение, которое удовлетворяет этой системе. По сути, это декларативное программирование, когда нам вообще не важно, как это будет работать, главное — результат.

Я еще несколько месяцев назад наискосок просмотрел немного документации (раз и два), но к практике на основе репозитория в итоге перешёл только в поезде без интернета, поэтому первые два задания я подглядел. В остальном все решалось достаточно просто, для решения задач нужно совсем немного конструкций.

В целом сама парадигма довольно прикольная: надушить четкое ТЗ и дело в шляпе (а недостаточно душнишь — держи тривиальное решение с нулями). Какое-нибудь судоку решать с помощью него — самое то, фигачится минут за 10. Да и задача о рюкзаке была реализована мной за примерно такое же время — это не динпрог вертеть.

Однако чудес солвер тоже не открыл. Магический квадрат для 4x4 он находит мгновенно, а вот 5x5 уже не смог (я не стал ждать больше 10 минут). При этом проц и память были вообще не нагружены, т.е. по умолчанию параллелизации нет. И рюкзак для «плохих» входных данных (где стоит приближенно решать) тоже быстро не отработал.

В общем, для чего-то простого, когда может человек решить с ручкой и бумагой за обозримое время или программист тупым перебором — вполне достойный вариант. Но если известен хороший алгоритм и задача не одноразовая, то стоит посмотреть альтернативы.