Stream: quantum computing

Topic: root


view this post on Zulip Anthony Bordg (Jul 29 2019 at 22:11):

@Josh Chen kindly added a root file for our future submission to the AFP.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC