xref: /plugin/mizarverifiabledocs/action.php (revision 1a91113b0094ce6ce10091527b530187a60781d5) 
1<?php
2// SPDX-License-Identifier: GPL-2.0-or-later
3// SPDX-FileCopyrightText: 2024-2025 Yamada, M.
4// DokuWiki Plugin Mizar Verifiable Docs (Action Component)
5
6use dokuwiki\Extension\ActionPlugin;
7use dokuwiki\Extension\EventHandler;
8use dokuwiki\Extension\Event;
9
10
11class action_plugin_mizarverifiabledocs extends ActionPlugin
12{
13    /* ===================== Register ===================== */
14
15    public function register(EventHandler $controller)
16    {
17        $controller->register_hook('AJAX_CALL_UNKNOWN', 'BEFORE', $this, 'handle_ajax_call');
18        $controller->register_hook('TPL_CONTENT_DISPLAY', 'BEFORE', $this, 'handle_tpl_content_display');
19    }
20
21    public function handle_tpl_content_display(Event $event, $_param)
22    {
23        if (!is_string($event->data)) return;
24
25        $html = $event->data;
26        if (strpos($html, 'mizarWrapper') !== false && strpos($html, 'id="hideAllButton"') === false) {
27            $buttonHtml = '<div class="hideAllContainer">'
28                        . '<button id="hideAllButton" class="hide-all-button">Hide All</button>'
29                        . '<button id="showAllButton" class="hide-all-button" style="display:none;">Show All</button>'
30                        . '<button id="resetAllButton" class="reset-all-button">Reset All</button>'
31                        . '</div>';
32            $event->data = $buttonHtml . $html;
33        }
34    }
35
36    public function handle_ajax_call(Event $event, $param)
37    {
38        unset($param);
39        switch ($event->data) {
40            case 'clear_temp_files':
41                $event->preventDefault(); $event->stopPropagation();
42                $this->clearTempFiles(); break;
43
44            case 'source_compile':
45                $event->preventDefault(); $event->stopPropagation();
46                $this->handleSourceCompileRequest(); break;
47
48            case 'source_sse':
49                $event->preventDefault(); $event->stopPropagation();
50                $this->handleSourceSSERequest(); break;
51
52            case 'view_compile':
53                $event->preventDefault(); $event->stopPropagation();
54                $this->handleViewCompileRequest(); break;
55
56            case 'view_sse':
57                $event->preventDefault(); $event->stopPropagation();
58                $this->handleViewSSERequest(); break;
59
60            case 'create_combined_file':
61                $event->preventDefault(); $event->stopPropagation();
62                $this->handle_create_combined_file(); break;
63
64            case 'view_graph':
65                $event->preventDefault(); $event->stopPropagation();
66                $this->handleViewGraphRequest(); break;
67        }
68    }
69
70    /* ===================== Helpers ===================== */
71
72    private function isWindows(): bool {
73        return strncasecmp(PHP_OS, 'WIN', 3) === 0;
74    }
75
76    /** 設定→未設定なら htdocs(= DOKU_INC の1つ上) 相対にフォールバックして正規化 */
77    private function resolvePaths(): array
78    {
79        // DokuWiki ルート（末尾スラッシュなしに正規化）
80        $dokuroot = rtrim(realpath(DOKU_INC), '/\\');
81
82        // htdocs を「dokuwiki の 1つ上」から求める
83        $htdocs = realpath($dokuroot . DIRECTORY_SEPARATOR . '..');
84        if ($htdocs === false) $htdocs = dirname($dokuroot);
85
86        $defM = $htdocs . DIRECTORY_SEPARATOR . 'MIZAR';
87        $defW = $htdocs . DIRECTORY_SEPARATOR . 'work';
88
89        // 設定値取得（空ならフォールバック）。相対指定が来たら htdocs 基準に解決
90        $exe   = trim((string)$this->getConf('mizar_exe_dir'));
91        $share = trim((string)$this->getConf('mizar_share_dir'));
92        $work  = trim((string)$this->getConf('mizar_work_dir'));
93
94        $isAbs = function(string $p): bool {
95            // Windowsドライブ/UNC/Unix ざっくり対応
96            return $p !== '' && (preg_match('~^[A-Za-z]:[\\/]|^\\\\\\\\|^/~', $p) === 1);
97        };
98
99        if ($exe   !== '' && !$isAbs($exe))   $exe   = $htdocs . DIRECTORY_SEPARATOR . $exe;
100        if ($share !== '' && !$isAbs($share)) $share = $htdocs . DIRECTORY_SEPARATOR . $share;
101        if ($work  !== '' && !$isAbs($work))  $work  = $htdocs . DIRECTORY_SEPARATOR . $work;
102
103        $exe   = rtrim($exe   ?: $defM, '/\\');
104        $share = rtrim($share ?: $defM, '/\\');
105        $work  = rtrim($work  ?: $defW, '/\\');
106
107        return ['exe' => $exe, 'share' => $share, 'work' => $work];
108    }
109
110    /** exeDir 直下 or exeDir\bin から実行ファイルを探す（.exe/.bat/.cmd 対応） */
111    private function findExe(string $exeDir, string $name): ?string
112    {
113        if ($this->isWindows()) {
114            $candidates = [
115                "$exeDir\\$name.exe",          "$exeDir\\bin\\$name.exe",
116                "$exeDir\\$name.bat",          "$exeDir\\bin\\$name.bat",
117                "$exeDir\\$name.cmd",          "$exeDir\\bin\\$name.cmd",
118                "$exeDir\\windows\\bin\\$name.exe",
119                "$exeDir\\win\\bin\\$name.exe",
120            ];
121        } else {
122            $candidates = [
123                "$exeDir/$name",               "$exeDir/bin/$name",
124            ];
125        }
126        foreach ($candidates as $p) {
127            if (is_file($p)) return $p;
128        }
129        return null;
130    }
131
132    /** 出力をUTF-8へ（WinはSJIS-WIN想定） */
133    private function outUTF8(string $s): string
134    {
135        return $this->isWindows() ? mb_convert_encoding($s, 'UTF-8', 'SJIS-WIN') : $s;
136    }
137
138    /**
139     * .exe は配列＋bypass_shell、.bat/.cmd は「cmd /C ""...""」の文字列＋shell経由で起動
140     * @return array [$proc, $pipes] 失敗時は [null, []]
141     */
142    private function openProcess(string $exeOrBat, array $args, string $cwd): array
143    {
144        $des = [1 => ['pipe','w'], 2 => ['pipe','w']];
145
146        if ($this->isWindows() && preg_match('/\.(bat|cmd)$/i', $exeOrBat)) {
147            // cmd /C ""C:\path\tool.bat" "arg1" "arg2""
148            $cmd = 'cmd.exe /C "'
149                 . '"' . $exeOrBat . '"';
150            foreach ($args as $a) {
151                $cmd .= ' ' . escapeshellarg($a);
152            }
153            $cmd .= '"';
154            $proc = proc_open($cmd, $des, $pipes, $cwd); // shell経由（bypass_shell=false）
155        } else {
156            $cmd = array_merge([$exeOrBat], $args);
157            $proc = proc_open($cmd, $des, $pipes, $cwd, null, ['bypass_shell' => true]);
158        }
159
160        if (!is_resource($proc)) return [null, []];
161        return [$proc, $pipes];
162    }
163
164    /* ===================== Source ===================== */
165
166    private function handleSourceCompileRequest()
167    {
168        global $INPUT;
169        $pageContent = $INPUT->post->str('content');
170        $mizarData = $this->extractMizarContent($pageContent);
171
172        if ($mizarData === null) { $this->sendAjaxResponse(false, 'Mizar content not found'); return; }
173        if (isset($mizarData['error'])) { $this->sendAjaxResponse(false, $mizarData['error']); return; }
174
175        $filePath = $this->saveMizarContent($mizarData);
176        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
177        $_SESSION['source_filepath'] = $filePath;
178
179        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
180    }
181
182    private function handleSourceSSERequest()
183    {
184        header('Content-Type: text/event-stream');
185        header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0');
186        header('Pragma: no-cache');
187        header('Expires: 0');
188
189        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
190        if (empty($_SESSION['source_filepath'])) {
191            echo "data: Mizar file path not found in session\n\n"; @ob_flush(); @flush(); return;
192        }
193
194        $this->streamSourceOutput($_SESSION['source_filepath']);
195
196        echo "event: end\n";
197        echo "data: Compilation complete\n\n";
198        @ob_flush(); @flush();
199    }
200
201    /* ===================== View ===================== */
202
203    private function handleViewCompileRequest()
204    {
205        global $INPUT;
206        $content = $INPUT->post->str('content');
207        $filePath = $this->createTempFile($content);
208
209        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
210        $_SESSION['view_filepath'] = $filePath;
211
212        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
213    }
214
215    private function handleViewSSERequest()
216    {
217        header('Content-Type: text/event-stream');
218        header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0');
219        header('Pragma: no-cache');
220        header('Expires: 0');
221
222        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
223        if (empty($_SESSION['view_filepath'])) {
224            echo "data: Mizar file path not found in session\n\n"; @ob_flush(); @flush(); return;
225        }
226
227        $this->streamViewCompileOutput($_SESSION['view_filepath']);
228
229        echo "event: end\n";
230        echo "data: Compilation complete\n\n";
231        @ob_flush(); @flush();
232    }
233
234    /***** view_graph: SVG を返す *****/
235    private function handleViewGraphRequest()
236    {
237        global $INPUT;
238        $content = $INPUT->post->str('content', '');
239        if ($content === '') { $this->sendAjaxResponse(false, 'Empty content'); return; }
240
241        $tmp = tempnam(sys_get_temp_dir(), 'miz');
242        $miz = $tmp . '.miz';
243        rename($tmp, $miz);
244        file_put_contents($miz, $content);
245
246        $parser = __DIR__ . '/script/miz2svg.py';
247        $py     = $this->getConf('py_cmd') ?: 'python';
248        $svg    = shell_exec(escapeshellcmd($py) . ' ' . escapeshellarg($parser) . ' ' . escapeshellarg($miz));
249        @unlink($miz);
250
251        if ($svg) $this->sendAjaxResponse(true, 'success', ['svg' => $svg]);
252        else      $this->sendAjaxResponse(false, 'conversion failed');
253    }
254
255    /* ===================== Content utils ===================== */
256
257    private function extractMizarContent($pageContent)
258    {
259        $pattern = '/<mizar\s+([^>]+)>(.*?)<\/mizar>/s';
260        preg_match_all($pattern, $pageContent, $m, PREG_SET_ORDER);
261        if (empty($m)) return null;
262
263        $fn   = trim($m[0][1]);
264        $stem = preg_replace('/\.miz$/i', '', $fn);
265        if (!$this->isValidFileName($stem)) {
266            return ['error' => "Invalid characters in file name: '{$stem}'. Only letters, numbers, underscores (_), and apostrophes (') are allowed, up to 8 characters."];
267        }
268
269        $combined = '';
270        foreach ($m as $mm) {
271            $cur = preg_replace('/\.miz$/i', '', trim($mm[1]));
272            if ($cur !== $stem) return ['error' => "File name mismatch in <mizar> tags: '{$stem}' and '{$cur}'"];
273            if (!$this->isValidFileName($cur)) return ['error' => "Invalid characters in file name: '{$cur}'."];
274            $combined .= trim($mm[2]) . "\n";
275        }
276        return ['fileName' => $stem . '.miz', 'content' => $combined];
277    }
278
279    private function isValidFileName($fileName)
280    {
281        if (strlen($fileName) > 8) return false;
282        return (bool)preg_match('/^[A-Za-z0-9_\']+$/', $fileName);
283    }
284
285    private function saveMizarContent($mizarData)
286    {
287        $paths = $this->resolvePaths();
288        $textDir = $paths['work'] . DIRECTORY_SEPARATOR . 'TEXT';
289        if (!is_dir($textDir)) @mkdir($textDir, 0777, true);
290
291        $filePath = $textDir . DIRECTORY_SEPARATOR . $mizarData['fileName'];
292        file_put_contents($filePath, $mizarData['content']);
293        return $filePath;
294    }
295
296    private function createTempFile($content)
297    {
298        $paths = $this->resolvePaths();
299        $textDir = $paths['work'] . DIRECTORY_SEPARATOR . 'TEXT';
300        if (!is_dir($textDir)) @mkdir($textDir, 0777, true);
301
302        $tempFilename = $textDir . DIRECTORY_SEPARATOR . str_replace('.', '_', uniqid('tmp', true)) . ".miz";
303        file_put_contents($tempFilename, $content);
304        return $tempFilename;
305    }
306
307    private function clearTempFiles()
308    {
309        $paths = $this->resolvePaths();
310        $dir = $paths['work'] . DIRECTORY_SEPARATOR . 'TEXT' . DIRECTORY_SEPARATOR;
311        $files = glob($dir . '*');
312
313        $errors = [];
314        foreach ($files as $f) {
315            if (is_file($f)) {
316                if (!$this->is_file_locked($f)) {
317                    $ok = false; $retries = 5;
318                    while ($retries-- > 0) { if (@unlink($f)) { $ok = true; break; } sleep(2); }
319                    if (!$ok) $errors[] = "Failed to delete: $f";
320                } else {
321                    $errors[] = "File is locked: $f";
322                }
323            }
324        }
325        if ($errors) $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors);
326        else         $this->sendAjaxResponse(true, 'Temporary files cleared successfully');
327    }
328
329    private function is_file_locked($file)
330    {
331        $fp = @fopen($file, "r+");
332        if ($fp === false) return true;
333        $locked = !flock($fp, LOCK_EX | LOCK_NB);
334        fclose($fp);
335        return $locked;
336    }
337
338    /* ===================== Run (miz2prel/makeenv/verifier) ===================== */
339
340    private function streamSourceOutput($filePath)
341    {
342        $paths = $this->resolvePaths();
343        $workPath  = $paths['work'];
344        $sharePath = $paths['share'];
345        putenv("MIZFILES={$sharePath}");
346
347        $exe = $this->findExe($paths['exe'], 'miz2prel');
348        if ($exe === null) {
349            echo "data: ERROR: miz2prel not found under {$paths['exe']} (or bin)\n\n"; @ob_flush(); @flush(); return;
350        }
351
352        [$proc, $pipes] = $this->openProcess($exe, [$filePath], $workPath);
353        if (!$proc) { echo "data: ERROR: Failed to execute miz2prel.\n\n"; @ob_flush(); @flush(); return; }
354
355        while (($line = fgets($pipes[1])) !== false) { echo "data: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
356        fclose($pipes[1]);
357        while (($line = fgets($pipes[2])) !== false) { echo "data: ERROR: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
358        fclose($pipes[2]);
359        proc_close($proc);
360
361        $errFilename = str_replace('.miz', '.err', $filePath);
362        $this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg');
363    }
364
365    private function streamViewCompileOutput($filePath)
366    {
367        $paths = $this->resolvePaths();
368        $workPath  = $paths['work'];
369        $sharePath = $paths['share'];
370        putenv("MIZFILES={$sharePath}");
371
372        // makeenv
373        $makeenv = $this->findExe($paths['exe'], 'makeenv');
374        if ($makeenv === null) { echo "data: ERROR: makeenv not found under {$paths['exe']} (or bin)\n\n"; @ob_flush(); @flush(); return; }
375        [$proc, $pipes] = $this->openProcess($makeenv, [$filePath], $workPath);
376        if (!$proc) { echo "data: ERROR: Failed to execute makeenv.\n\n"; @ob_flush(); @flush(); return; }
377        while (($line = fgets($pipes[1])) !== false) { echo "data: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
378        fclose($pipes[1]);
379        while (($line = fgets($pipes[2])) !== false) { echo "data: ERROR: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
380        fclose($pipes[2]);
381        proc_close($proc);
382
383        $errFilename = str_replace('.miz', '.err', $filePath);
384        if ($this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg')) return;
385
386        // verifier
387        $verifier = $this->findExe($paths['exe'], 'verifier');
388        if ($verifier === null) { echo "data: ERROR: verifier not found under {$paths['exe']} (or bin)\n\n"; @ob_flush(); @flush(); return; }
389        $rel = 'TEXT' . DIRECTORY_SEPARATOR . basename($filePath);
390        [$proc, $pipes] = $this->openProcess($verifier, ['-q','-l',$rel], $workPath);
391        if (!$proc) { echo "data: ERROR: Failed to execute verifier.\n\n"; @ob_flush(); @flush(); return; }
392        while (($line = fgets($pipes[1])) !== false) { echo "data: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
393        fclose($pipes[1]);
394        while (($line = fgets($pipes[2])) !== false) { echo "data: ERROR: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
395        fclose($pipes[2]);
396        proc_close($proc);
397
398        $this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg');
399    }
400
401    /* ===================== Errors ===================== */
402
403    private function getMizarErrorMessages($mizarMsgFile)
404    {
405        if (!is_file($mizarMsgFile)) return [];
406        $errorMessages = [];
407        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
408        $isReading = false; $key = 0;
409        foreach ($lines as $line) {
410            if (preg_match('/# (\d+)/', $line, $m)) { $isReading = true; $key = (int)$m[1]; }
411            elseif ($isReading) { $errorMessages[$key] = $line; $isReading = false; }
412        }
413        return $errorMessages;
414    }
415
416    private function handleCompilationErrors($errFilename, $mizarMsgFilePath)
417    {
418        if (!file_exists($errFilename)) return false;
419        $errs = []; $lines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
420        foreach ($lines as $ln) {
421            if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $ln, $m)) {
422                $code = (int)$m[3];
423                $errs[] = [
424                    'code'    => $code,
425                    'line'    => (int)$m[1],
426                    'column'  => (int)$m[2],
427                    'message' => $this->getMizarErrorMessages($mizarMsgFilePath)[$code] ?? 'Unknown error'
428                ];
429            }
430        }
431        if ($errs) {
432            echo "event: compileErrors\n";
433            echo "data: " . json_encode($errs) . "\n\n";
434            @ob_flush(); @flush();
435            return true;
436        }
437        return false;
438    }
439
440    private function sendAjaxResponse($success, $message, $data = '')
441    {
442        header('Content-Type: application/json');
443        header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0');
444        header('Pragma: no-cache');
445        header('Expires: 0');
446        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
447        exit;
448    }
449
450    private function handle_create_combined_file()
451    {
452        global $INPUT;
453        $combinedContent = $INPUT->post->str('content');
454        $filename = $INPUT->post->str('filename', 'combined_file.miz');
455
456        if (!empty($combinedContent)) {
457            $this->sendAjaxResponse(true, 'File created successfully', [
458                'filename' => $filename,
459                'content'  => $combinedContent
460            ]);
461        } else {
462            $this->sendAjaxResponse(false, 'Content is empty, no file created');
463        }
464    }
465}
466