TODO List

[Jazzpirate]

• git update seems to not work anymore
  • still wrong; (checkout => "1 commit ahead of origin"???)
• Images in Documents
• JSON export problems
  • IDE support
• Gottos
• Slides endpoint
• standalone tex packaging (IDE)
• Another "the sandboxed-arenas feature is active, but no Arena is active" crash (reactive_graph/src/owner/arena.re:60:29)
• All-stale build queue
• timeouts for SPARQL queries
• refactor router/crates for compilation speed
• dataabse config seems to be ignored?
• PDF download
• What are Morphisms?
  • Morphisms in FLAMS!
• sTeX
  • Use CSS for things that should use CSS
  • multiple MathHub directories
  • sref
• Semantics Extraction
  • Ignore comments
• LSP
  • VSCode links in build queue
  • Server
    • linting rules for various macros
    • problems
    • precondition / objectives
    • proofs => induce definientia
  • VSCode Client
    • download archives
      • download dependencies
• build queue / IDE integration(?)
• search
  • IDE
• GitLab Integration
• Build system
  • finished queue state
  • sandboxing
• shtml-viewer
  • proper hovers
  • collapsible proofs
  • slideshows
• OMDoc rendering
• proper (de)serialization of datastructures
  • => proper interlinking
• git(lab) integration

[kohlhase]

I would like the linter to warn me of overcommitted \importmodule{foo} or \usemodule{foo}: in the current situation none of the local declarations of module foo are used. Quick fix: replace \...module{foo} by all the imports of module foo (possibly changed to \usemodule).

[Jazzpirate]

I see some issues with this, in particular if we consider best practice to be to keep dependencies minimal. I'm almost sure that in the AI notes (at least in my rewrites of AI2), it is often the case that slides build on each other; not necessarily because a symbol of some module is actually used, but also because "that slide came before this one, so I know it already includes all the things I will need".
One thing I've already done there was to make a convenience module whose only reason to exist is to export quite a few other modules, so I don't have to have 10 importmodules at the beginning of each slide in some section. The latter is of course counter to "keeping dependencies minimal", but also quite convenient.
Which is to say: I would expect having such a warning to yield quite a few positives which may or may not be annoying if they're intentional (which they may often be).
I think we should clarify what best practices regarding imports, redundant imports, spurious imports etc. actually should be given various up- and downsides...

[kohlhase]

I agree with all you say, and let me answer some of the concerns above as a step towards "best practices".
Generally: when in doubt, I am for more information, then I can decide.

Also I probably meant the info (blue in VSCode) when I said "should warn me" above.

As for the convenience module, I would consider this as "good practice" to use that for writing (makes life easy as you say) and then when the dust of writing and using the first time has settled, then we can refine the convenience import to the minimal one, thus minimizing dependencies.

You also mention imports that "that slide came before this one, so I know it already includes all the things I will need". This is also something I see a lot, and I have been worrying about this (without coming to a specific conclusion or even doing something about it). I am wondering whether that should be be refactored into two properties:

1. "this slide should come after that one because it systematically builds on it"
2. "this module imports that module".

ad 1.: this seems to be a rethoric/didactic relation, and maybe we want to have a specific sTeX markup for this relation in the future.
ad 2. this is just the "convenience import" from above which could safely be refined.
I actually quite like this idea; especially, if the refactoring could be supported by the IDE.

[kohlhase]

BUT I just realize one Problem with my proposal. If we minimize the imports of one module, we might compromize all modules that import from it. This makes it a global operation rather than a local one. I wonder whether we should split the VSCode IDE into two. One with essentially just the linter (for all the local stuff) and a Curation IDE that does the global stuff like quickparse with an extended curation linter.

[Jazzpirate]

true - which reinforces my point from recently: I think redundant imports are good, actually; both because they make dependencies explicit and because it makes them more robust against import-refactoring of dependencies...