@rustlang_ru - страница 173

分解物質

ещё у clang есть бесплатный но проще

Danila Matveev

че-то верификацию усиленно путают с анализаторами

Berkus

ну можно хотябы формально верифицировать https://wiki.sel4.systems/FrequentlyAskedQuestions#What_does_seL4.27s_formal_verification_mean.3F

нельзя, в seL4 верифицируется очень узкий сабсет

Berkus

ну и чтобы тебе было смешнее - в seL4 все алгоритмы сначала кодируются на хаскеле

Berkus

че-то верификацию усиленно путают с анализаторами

ага, хотя совсем разные вещи

Vladimir

Например это делается на более низком уровне, уже llvm этим занимается, и мы вообще говорили о либе syn которая содержит только парсер токенов.

LexsZero

> after initialization

分解物質

нельзя, в seL4 верифицируется очень узкий сабсет

где такое написано?

Berkus

в сорцах

分解物質

the proof currently is about the operation of the kernel after it has been loaded correctly into memory and brought into a consistent, minimal initial state. This leaves out about 1,200 lines of the code base that a kernel programmer would usually consider to be part of the kernel.

分解物質

the proof currently is about the operation of the kernel after it has been loaded correctly into memory and brought into a consistent, minimal initial state. This leaves out about 1,200 lines of the code base that a kernel programmer would usually consider to be part of the kernel.

отсюда http://sel4.systems/Info/FAQ/proof.pml

Berkus

это не про то

分解物質

the proof currently is about the operation of the kernel after it has been loaded correctly into memory and brought into a consistent, minimal initial state. This leaves out about 1,200 lines of the code base that a kernel programmer would usually consider to be part of the kernel.

т.е. покрывает все действия ядра сразу после загрузки

Berkus

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

Berkus

мало того, на сегодняшний день верифицирован код даже не под все поддерживаемые архитектуры

Berkus

если тебе лениво искать в сорцах - поройся в мейлинг листе, там Герно отвечает на такие вопросы регулярно

分解物質

ясн

Emerald

А ну-ка вопрос: Кто-нибудь делал каллбеки на расте, как вы это делали? Как засунуть ссылку на функцию или замыкание в структуру ?

Anonymous

ненад каллбеки делать

Anonymous

есть фючюры

Emerald

Вам не нравится что калбеки подразумевают реверс control flow ?

Emerald

Я пока что сделал без калбека, просто loop { let event = MyAPI.pump_event() ...

Emerald

Можно наверное у всех асинхронных штук сделать такие качалки событий и в своём main loop собирать их и считать какую-то логику. 🤔

Anonymous

или использовать нормальную асинк либу :/

Anonymous

но если очень нужно то есть трейт Fn

Emerald

но если очень нужно то есть трейт Fn

Уже пытался и споткнулся о lifetimes

Anonymous

fn my_func<F>(f: F) where F: Fn(i32) -> i32, { }

Anonymous

как-то так

Emerald

Это тип функция высшего порядка? А как в struct засунуть поле-колбек которое можно в любой момент вызвать?

Anonymous

Это тип функция высшего порядка? А как в struct засунуть поле-колбек которое можно в любой момент вызвать?

ну как-бы да

доня.

@luciuslapis почему ты так упорно не хочешь использовать фьючеры?

Anonymous

чтоб засунуть функцию в struct она должна быть в Box

Emerald

@luciuslapis почему ты так упорно не хочешь использовать фьючеры?

Чистый язык использовать хочется, да и future разве не однократные вычисления? Подразумевается что каждый раз надо брать новый future ?

Anonymous

struct MyStruct<F: Fn() -> () + 'static> { param: Box<F> }

Anonymous

вроде

Anonymous

Чистый язык использовать хочется, да и future разве не однократные вычисления? Подразумевается что каждый раз надо брать новый future ?

нет, не однократные

Мерль

А ну-ка вопрос: Кто-нибудь делал каллбеки на расте, как вы это делали? Как засунуть ссылку на функцию или замыкание в структуру ?

struct Struct<T> { f: Box<Fn()->T+ 'static, }

Мерль

struct Struct<T> { f: Box<Fn()->T+ 'static, }

Например так

Anonymous

с фючюрами намного приятнее код будет

Мерль

struct MyStruct<F: Fn() -> () + 'static> { param: Box<F> }

Лол

Emerald

с фючюрами намного приятнее код будет

Ок учту, спасибо за пример

Alex

фьючуры требуют реактора

Anonymous

struct Struct<T> { f: Box<Fn()->T+ 'static, }

почему это работает в стракте но не как аргумент функции?

Emerald

Сделал так https://play.rust-lang.org/?gist=98fe260714aca7de1d0acfb99a97b47e&version=stable

Emerald

Вот хороший ответ, продолжу разбираться по нему https://stackoverflow.com/questions/41081240/idiomatic-callbacks-in-rust

Anonymous

хм, а в последней версии раста замыкания же могут коерситься в поинтеры функций

Emerald

хм, а в последней версии раста замыкания же могут коерситься в поинтеры функций

верно, видел в чейннджлоге https://github.com/rust-lang/rfcs/pull/1558/files/d51becd78f00e89e7fef6c21cd5a61075e2026ca

Emerald

Где бы хороший гайд по замыканиям в расте взять

Emerald

верно, видел в чейннджлоге https://github.com/rust-lang/rfcs/pull/1558/files/d51becd78f00e89e7fef6c21cd5a61075e2026ca

https://blog.rust-lang.org/2017/07/20/Rust-1.19.html тут

Anton

Кстати, мне тоже интересно, как в расте с асинхронностью работают, не добрался ещё до этого

Anton

Когда какой-нибудь простой update loop делаешь

Anton

Там же наверное всё в мьютексы придётся оборачивать?

Emerald

Пока что в своём IRC-боте я просто делаю блокающие read из сокета, и свой main loop со sleep. Самое простое решение.

Мерль

почему это работает в стракте но не как аргумент функции?

Почему это не работает как аргумент? Всё прекрасно работает Или я тебя не понял

Anonymous

хм

Emerald

Там же наверное всё в мьютексы придётся оборачивать?

Если делать асинхронность за счёт другого треда или тредпула то придётся видимо, либо с мьютексами либо вот так https://doc.rust-lang.org/std/sync/mpsc/

Anton

Если делать асинхронность за счёт другого треда или тредпула то придётся видимо, либо с мьютексами либо вот так https://doc.rust-lang.org/std/sync/mpsc/

Не, если через один тред

Anonymous

я поехал тогда

Мерль

хм

https://play.rust-lang.org/?gist=f75f1e3519c30f11ba343e06ad760f1d&version=nightly

Anonymous

https://play.rust-lang.org/?gist=f75f1e3519c30f11ba343e06ad760f1d&version=nightly

ну, здесь оно как генерик

Anonymous

а в стракте этого не надо

Emerald

Не, если через один тред

Я вот и думаю запустить отдельный IO тред, к нему канал mpsc, но как поставить control flow с ног на голову чтобы не я читал из канала а канал вызывал обработчики? Пока что опять вижу только решение с main loop, опросом всех каналов и sleep

Мерль

ну, здесь оно как генерик

Нет проблемы просто ручками заменить на нужный тип, если дженерик не нужен, разве нет?

Anonymous

нани

Anonymous

я спрашиваю почему в стракте можно без генерика

Мерль

я спрашиваю почему в стракте можно без генерика

Дык и в функции можно

Мерль

Или я не прав?

Anton

Я вот и думаю запустить отдельный IO тред, к нему канал mpsc, но как поставить control flow с ног на голову чтобы не я читал из канала а канал вызывал обработчики? Пока что опять вижу только решение с main loop, опросом всех каналов и sleep

Я так понимаю, это в принципе невозможно. У тебя либо pull-модель, где ты разбираешь очередь, либо push, когда у тебя новый поток выполнения рождается в каком-то контексте. И этот контекст, естественно, борроуит переменные

Anonymous

так Fn же трейт

Anonymous

🤔🤔🤔

Мерль

так Fn же трейт

Я видимо не выспался Ты не мог бы объяснить свою мысль для тупых? Я никак не могу уловить суть твоих сомнений (

Anonymous

ну Fn это не тип, а trait

Мерль

Да

Anonymous

потому в функции он должен быть написан через генерики, так?

Мерль

Аааа

Мерль

Блин

Мерль

Хммм

Мерль

потому в функции он должен быть написан через генерики, так?

А ты не мог бы попробовать сделать не через дженерик и показать выхлоп? Я не могу, у меня л̶а̶п̶к̶и̶ смартфон только под рукой, с ним play rust не пашет

Anonymous

нет, поэтому я и спрашиваю

Anonymous

потому в функции он должен быть написан через генерики, так?

по-сути тоже самое и со страктами