-
Notifications
You must be signed in to change notification settings - Fork 231
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Documentation, tutorials, libraries, etc. #1566
Comments
Linking to #1543 too. Also, I think we should start sending announcements on features/improvements to the mailing list instead of Slack. |
Notes from a discussion at a group meeting today regarding improving the F* library: What kinds of improvements do we foresee?
How do we get there?We hope to make some concrete progress in the next month, presenting improvements to specific modules as exemplars to follow for the rest
|
A proposed revised directory structure (work in progress)
See the table in https://github.com/FStarLang/FStar/wiki/Documenting-the-library |
While we are at it, should we also rename |
Renaming |
I was thinking yesterday that the per-functionality split (core, native, math, etc) should probably not be made into directories. It makes it harder to find a module when you know its name (but maybe not its class) and pollutes the include paths (+ introduces a question of precedence). If the only reason for this is to make it easier to discover related functionality, perhaps we need to write and maintain a "roadmap" file, or some kind of marker within each file so they can be listed automatically. The legacy/experimental split into directories does make sense to me, I would expect them to be left out of the include paths and manually added by users if needed, so they know they are doing something fishy. I would not mind however to use the directory structure to match the module's namespaces, à la Agda/Haskell. |
The proposal was based on the observation that fsdoc doesn't render nicely when running a file through fstlit. So, right now, this makes it hard to mix fslit and fsdoc together. The suggestion was to make fslit aware of fsdoc so that when rendering a file via fslist, fsdoc summaries get interpreted as, say, bold text, and the body of fsdoc gets intepreted as regular restructured text. |
Is that table editable in place for others? If not, maybe I should move it to a wiki page where we can all edit. Some responses to points raised so far:
We also have the Steel namespace in another branch. What convention does it represent? |
As for |
As @mtzguido, I believe that splitting files into subdirectories introduces more problems than it solves. It adds new default include paths and creates confusion about their precedence. It also makes it harder to find a module and grep in files. The only advantage I see is that it unclutters It still makes sense to move legacy and experimental modules into subdirectories not in the default include path so as to force users of those modules to be conscious about their nature. I would have a different opinion if there was some relation between filesystem paths and module names, like in Haskell/Agda/Coq (see e.g. https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#libraries-and-filesystem). A last concern about a massive module renaming is upgrading existing code and annoying users. I think it wouldn't take much effort to keep backwards compatibility by preserving existing modules: e.g. if we split |
About a massive module renaming: yes, I was thinking of something like you proposed to not break everyone. The module with the old name would include the new ones, go in the |
Note that |
Are we proposing subdirectories as a substitute for a README.md or a bit of high-level documentation that would give a tour of ulib, presenting each module and giving a one-sentence summary of what they're supposed to achieve? This was the intent behind https://fstarlang.github.io/docs/ -- would a more structured version of that landing page suffice? I am still in favor of moving legacy and experimental files in subdirectories because the intent is that these files should not be discoverable. |
Some comments ahead of the discussion:
|
For reference, here's the (documentation) style guide that is enforced by Python for their libraries: https://www.python.org/dev/peps/pep-0257/ |
Folks, from #1854 it seems pretty clear to me that we need to significantly improve fsdoc in order to use it to generate reasonably formatted documentation independently from the code of our libraries. My concern now is that we'll be unable or unwilling to document our libraries until the fsdoc tool improves. Should we just go ahead and document our libraries in code comments associated with every signature. You can browse the documentation locally, of course, or online using linguist in a browser to make it look at least somewhat pretty. Welcoming opinions from all, pinging a few. @protz @ad-l @aseemr @denismerigoux @jaybosamiya |
For generating documentation, would we be better off writing a separate text-processing tool to emit selected parts of a F* module in markdown? The current |
Isn't it what |
yep, that's the fslit model. I'm asking if it makes sense for fsdoc to be similar. |
I would be in favor of not gating the documentation on improvements of |
Yup, documentation improvements don't need to depend on having improvement on fsdoc yet. If we follow the style that @denismerigoux and I have written for #1854, then it should(?) be fairly straightforward to write a separate tool that can generate markdown/html that looks nice. For an example of how I expect the tool to generate markdown/html output, see the comment there (or alternatively https://gist.github.com/jaybosamiya/05f28d6e34c45b73436a835031346c77 which has working hyperlinks too). |
See Issue #90 for some other ideas about extending the tutorial |
See issue #88 for some ideas about marking up and extracting documentation from F* files |
Would be nice to have a dedicated tutorial chapter regarding normalization |
We've been discussing about consolidating F* libraries, documenting them, refreshing our tutorials etc. in the coming months, e.g., by April 2019. The requirements for this are pretty open ended. Let's use this issue to discuss goals, non-goals and work items towards this task.
Other things?
Please weigh in with your hopes and desires for documentation.
So far, the discussion included the following people:
@aseemr @mtzguido @protz @tahina-pro @catalin-hritcu @danelahman @zoep
The text was updated successfully, but these errors were encountered: