Anthony Bordg (Jul 29 2019 at 22:11): Anthony Bordg (Jul 29 2019 at 22:11):@Josh Chen kindly added a root file for our future submission to the AFP.
Josh Chen (Jul 29 2019 at 22:16):It's nothing, I merely started reading through the theories more closely and wanted to organize some things. (Actually the added ROOT file isn't yet up to AFP standard, it still needs a label after the session name and a timeout option.)
Anthony Bordg (Jul 29 2019 at 22:22):@Hanna Lachnitt @Yijun He when you open a PR to add a new theory please also update the root file accordingly.
Anthony Bordg (Jul 29 2019 at 22:27):It's nothing, I merely started reading through the theories more closely and wanted to organize some things. (Actually the added ROOT file isn't yet up to AFP standard, it still needs a label after the session name and a timeout option.)
I added the label after the session name.
Anthony Bordg (Jul 29 2019 at 22:35):@Josh Chen
Just to understand: does it mean that when a user will browse our theories, the sessions it's based on, namely Jordan_Normal_Form.thy (top-level), Matrix_Tensor and VectorSpace will be unavailable for processing (coloured in pink).
Josh Chen (Jul 29 2019 at 22:40):the sessions it's based on, namely Jordan_Normal_Form.thy (top-level), Matrix_Tensor and VectorSpace will be unavailable for processing
This will happen when Isabelle_marries_Dirac is chosen as a session. Otherwise, what is available for processing depends on the session chosen. Basically (as far as I understand) choosing some session S makes S and all its imported sessions unavailable, since Isabelle uses the built images instead of processing the theory files. But any other dependency not included as a session import will be processed.
Anthony Bordg (Jul 29 2019 at 22:57):@Josh Chen it would be a great contribution to #general if you open a topic there and explain how a session is chosen, how this affects the processing and the consequences.
Last updated: Nov 23 2024 at 04:23 UTC