Dacit

6 ms·

1. 1.▲
   by Dacit 2mo ago

   You will want at least a separate session for the `restricteduser`: E.g. with X11, a process in the same session can do almost anything with your input/output. And most Linux distributions make it really hard to disable external devi
2. 2.▲
   by Dacit 2mo ago

   >(FWIW) Gemini agrees LLM hallucination: Poly/ML has been in use since at least 1986 (see e.g. Paulsons preliminary user's manual for Isabelle).
3. 3.▲
   by Dacit 7mo ago

   You are clearly misinformed. According to German law, you can start a UG (limited) with only 1€ + notary cost. Starting a business with personal liability doesn't cost anything.
4. 4.▲
   by Dacit 7mo ago

   No. The whole point of the LCF approach is that only kernel functions can generate theorems. Usually this is done by having a Thm module with opaque thm type (so its instances can only be generated by this module) and embedding the base rul
5. 5.▲
   by Dacit 7mo ago

   In the described case, this was a simple user error. But you are right nonetheless: To enable the concurrency, the system uses a parallel inference kernel ( https://www21.in.tum.de/~wenzelm/papers/parallel-isabelle.
6. 6.▲
   by Dacit 7mo ago

   Indeed this can simply be checked by a command-line invocation. But I don't think the student was aware: They would only have seen a purple coloring of the "stuck" part, as shown in the linked example in the blog post. And if