Zulip Chat Archive

Stream: FLT-regular

Topic: dependency graph

Riccardo Brasca (Jun 02 2022 at 11:09):

I am updating the blueprint, the first section is done. In the graph, I don't understand why alt_definition_of_norm is not green, even if its proof has leanok. @Chris Birkbeck do you have any idea?

Alex J. Best (Jun 02 2022 at 11:47):

Looks green to me, did you fix it? Maybe it was just slow to update

Riccardo Brasca (Jun 02 2022 at 12:09):

I've switched the order of alt_definition_of_norm and alt_definition_of_trace in the tex file, and now alt_definition_of_trace (the first one in the tex) is not green. And also it's not connected, but it used in the blueprint. :thinking:

Riccardo Brasca (Jun 02 2022 at 14:18):

Also prop:discr_of_cyclo does not appear in the graph.

Chris Birkbeck (Jun 03 2022 at 08:00):

I'll have a look later today and see if I can make them show up correctly

Chris Birkbeck (Jun 03 2022 at 10:46):

Riccardo Brasca said:

Also prop:discr_of_cyclo does not appear in the graph.

This is showing up now. The issue is that the dep graph doesn't like things being propositions.

Riccardo Brasca (Jun 03 2022 at 10:47):

Ah, good to know!

Chris Birkbeck (Jun 03 2022 at 10:48):

But I still dont know why alt_definition_of_trace doesn't show up correctly.

Riccardo Brasca (Jun 03 2022 at 10:49):

It is something related to being the first lemma. I mean, if you switch trace with norm, then trace is OK and norm is not green.

Chris Birkbeck (Jun 03 2022 at 10:51):

Hmm weird

Patrick Massot (Jun 03 2022 at 13:02):

Chris Birkbeck said:

Riccardo Brasca said:

Also prop:discr_of_cyclo does not appear in the graph.

This is showing up now. The issue is that the dep graph doesn't like things being propositions.

More precisely, it doesn't like prop, whereas proposition is ok, as can be seen at https://github.com/PatrickMassot/leanblueprint/blob/master/leanblueprint/Packages/blueprint.py#L40. The easiest fix is to rename thing to proposition but you can also use the coverage_thms package option to change this list.

Chris Birkbeck (Jun 03 2022 at 13:04):

Oh I didn't know proposition worked! Great. I had used this for some of my lecture notes and wanted to do a dep graph, but since I couldn't get props to work (and I didn't want to make everything a lemma) I had given up!

Patrick Massot (Jun 03 2022 at 13:15):

I'm sorry about the lack of documentation.

Chris Birkbeck (Jun 03 2022 at 13:16):

Don't be! I was just lazy and didn't bother asking

Patrick Massot (Jun 03 2022 at 13:18):

One trick you could have used would have been to look at the sphere eversion or liquid repo and see there are lots of propositions there.

Riccardo Brasca (Jun 02 2022 at 11:09):

I am updating the blueprint, the first section is done. In the graph, I don't understand why alt_definition_of_norm is not green, even if its proof has leanok. @Chris Birkbeck do you have any idea?

Alex J. Best (Jun 02 2022 at 11:47):

Looks green to me, did you fix it? Maybe it was just slow to update

Riccardo Brasca (Jun 02 2022 at 12:09):

I've switched the order of alt_definition_of_norm and alt_definition_of_trace in the tex file, and now alt_definition_of_trace (the first one in the tex) is not green. And also it's not connected, but it used in the blueprint. :thinking:

Riccardo Brasca (Jun 02 2022 at 14:18):

Also prop:discr_of_cyclo does not appear in the graph.

Chris Birkbeck (Jun 03 2022 at 08:00):

I'll have a look later today and see if I can make them show up correctly

Chris Birkbeck (Jun 03 2022 at 10:46):

Riccardo Brasca said:

Also prop:discr_of_cyclo does not appear in the graph.

This is showing up now. The issue is that the dep graph doesn't like things being propositions.

Riccardo Brasca (Jun 03 2022 at 10:47):

Ah, good to know!

Chris Birkbeck (Jun 03 2022 at 10:48):

But I still dont know why alt_definition_of_trace doesn't show up correctly.

Riccardo Brasca (Jun 03 2022 at 10:49):

It is something related to being the first lemma. I mean, if you switch trace with norm, then trace is OK and norm is not green.

Chris Birkbeck (Jun 03 2022 at 10:51):

Hmm weird

Patrick Massot (Jun 03 2022 at 13:02):

Chris Birkbeck said:

Riccardo Brasca said:

Also prop:discr_of_cyclo does not appear in the graph.

This is showing up now. The issue is that the dep graph doesn't like things being propositions.

More precisely, it doesn't like prop, whereas proposition is ok, as can be seen at https://github.com/PatrickMassot/leanblueprint/blob/master/leanblueprint/Packages/blueprint.py#L40. The easiest fix is to rename thing to proposition but you can also use the coverage_thms package option to change this list.

Chris Birkbeck (Jun 03 2022 at 13:04):

Oh I didn't know proposition worked! Great. I had used this for some of my lecture notes and wanted to do a dep graph, but since I couldn't get props to work (and I didn't want to make everything a lemma) I had given up!

Patrick Massot (Jun 03 2022 at 13:15):

I'm sorry about the lack of documentation.

Chris Birkbeck (Jun 03 2022 at 13:16):

Don't be! I was just lazy and didn't bother asking

Patrick Massot (Jun 03 2022 at 13:18):

One trick you could have used would have been to look at the sphere eversion or liquid repo and see there are lots of propositions there.

Last updated: Dec 20 2023 at 11:08 UTC