Как сделать многопоточную многопоточность в Isabelle ML?

Я нашел использование для того, чтобы начать несколько процессов Isabelle_System.bash.Как сделать многопоточную многопоточность в Isabelle ML?

В этом следующем источнике я использую команды 3 bash. Для простого примера я хотел бы запустить их в отдельных потоках, чтобы они запускались одновременно, а не последовательно.

ML {* 
Isabelle_System.bash ("echo '1. Call script to compile in the PIDE console.'"); 
Isabelle_System.bash ("echo '2. Call script to compile in a Windows console.'"); 
Isabelle_System.bash ("echo '3. Maybe a third process.'"); 
(*In an outer syntax command, I have options to allow 1 and 2, so it might be 
    useful to allow starting both at the same time, to be able to terminate the 
    PIDE process, and let the Windows console keep running. But, unless 
    multithreading is used, their execution will be sequential, which is 
    useless.*) 
*}

Я сделал Grep, и я нашел src/Pure/Concurrent/simple_thread.ML.

Однако это не приоритет, и для меня было бы нецелесообразно использовать пробные ошибки, чтобы попытаться выяснить, что нужно делать самостоятельно.

Если кто-то может дать мне простой шаблон plug-n-play для запуска 3 команд bash выше, я был бы признателен. Или, может быть, кто-то может сказать мне, почему я не могу или не должен этого делать.

источник

2014-10-27 Anonymous

«Простая многопоточность» - это оксюморон, потому что нитки никогда не просты. Если вы просто хотите сделать параллельное программирование, что просто, то первое, что нужно посмотреть, это структура Par_List, например. Комбинатор Par_List.map. В Isabelle/Isar Implementation Manual есть раздел «Параллельные скелеты» об этом, а также дополнительная информация поблизости.

источник

2014-10-28 08:02:39 Makarius

Макарий, как правило, это лучше, чтобы не кусать руку, которая кормит меня, но ... Вот, вы делаете случайный комментарий, или вы выкладывал мне на языке. Я воспринимаю это как лекцию, так как вы делаете это с помощью языка. Вы выбираете язык, который заставляет людей думать определенным образом (основная проблема заключается в том, что вы выбираете то, что уже имеет широко распространенное значение), а затем вы говорите людям, чтобы они не думали так. Это как сказать собаке, чтобы не помахать хвостом. Вы назвали структуру SIMPLE_THREAD. Иногда я пытаюсь подчиниться, даже когда я не согласен. Будучи новичком, я следовал примеру профессионала. Посмотри, что случилось. –

Теперь я вижу, что имя внутренней структуры Simple_Thread может привести к путанице. Он был мотивирован как слегка упрощенная оболочка над основными структурами Thread, как в ML, так и в JVM. Как правило, когда человек обнаруживает что-то потенциально полезное, быстрый гиперпоиск для его типичных применений дает представление о его значимости для приложений. – Makarius

Здесь я запишу несколько деталей, основываясь на ответе Макария Венцеля.

Оказывается, что с библиотекой Isabelle/ML в И/Pure, работает параллельно, независимые процессы Баша чрезвычайно легко:

ML {* (*Running this multiple times shows the order of execution varies.*) 
    Par_List.map : ('a -> 'b) -> 'a list -> 'b list; 
    val bash_strings = [ 
    "echo 'Echo 1.'; echo 'Echo 1.'; echo 'Echo 1.'; echo 'Echo 1.' ", 
    "echo 'Bash 2, bro!'", 
    "echo 'Bash 3, hombre or señorita!'", 
    "echo 'Bash 4, dude!'"]; 
    val _ = Par_List.map Isabelle_System.bash bash_strings 
*} (* 
OUTPUT: 
    Bash 4, dude! 
    Bash 2, bro! 
    Bash 3, hombre or señorita! 
    Echo 1. 
    Echo 1. 
    Echo 1. 
    Echo 1. 
    val it = fn: ('a -> 'b) -> 'a list -> 'b list 
    val bash_strings = 
    ["echo 'Echo 1.'; echo 'Echo 1.'; echo 'Echo 1.'; echo 'Echo 1.' ", 
     "echo 'Bash 2, bro!'", "echo 'Bash 3, hombre or señorita!'", 
     "echo 'Bash 4, dude!'"]: 
    string list*)

5-минутное решение проблемы реализации в несколько месяцев, не подсчитывая накладные расходы, задавая вопрос, читая ответ, открывая PDF-файл, запуская PIDE и набирая различные материалы, прежде чем блокировать какой-то источник, который показывает простой пример, который работает.

источник

2014-10-28 14:17:23

Как сделать многопоточную многопоточность в Isabelle ML?

ответ

Смежные вопросы