Skip to content
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

TUTORIALS: Reorganise tutorials and add inline solutions #106

Open
wants to merge 178 commits into
base: master
Choose a base branch
from

Conversation

bbrcknl
Copy link

@bbrcknl bbrcknl commented May 27, 2024

The updates in this PR were written in conjunction with those in seL4/docs#231

The aim of both PRs is:

To arrange the tutorial material on the docsite such that it is clear and easy to follow. Inspired by the Rust book https://doc.rust-lang.org/book/, the user can see the chapters in the index on the left, and go straight to the sections that they need.

Specifically, the updates on the docsite provide:

  • a streamlined guide to completing the tutorials
  • a streamlined "setting up your machine" page
  • a how-to page with solutions to tutorial questions
  • more organised landing page

The tutorials have been slightly rewritten to:

  • correct minor errors
  • provide inline solutions for readers wishing to understand the material and/or get quick solutions

Remaining issues:

  • camkes-timer part 2 fails to compile (ninja) with current solutions - need someone with know-how to check what's going on
  • I didn't test camkes-vm-linux; wasn't sure whether to spend a lot of time investigating KVM alternative for Mac
  • the tutorial camkes-vm-crossvm fails to initialise - need someone with know-how to check what's going on

A note on using the rewritten docsite (from seL4/docs#231):
While the docsite in this PR has the new tutorial layout, the Makefile clones the old tutorials from https://github.com/seL4/sel4-tutorials.

You’ll need to integrate the updated tutorials (from this PR) in the Makefile from seL4/docs#231
I can’t offer code for this because I’m a Makefile noob. I tested the new tutorials by having the Makefile call in and manipulate tutorial files from local directories.

bbrcknl and others added 30 commits April 19, 2024 11:51
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
bbrcknl added 2 commits July 29, 2024 16:51
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Copy link

@Indanz Indanz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Other than changing copyright holders, overall it seems fine. I haven't seen it rendered yet though.


```
/*-- filter TaskContent("hello", TaskContentType.BEFORE, subtask="event-task3") -*/
/* TASK 3: the event interfaces */
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure about the discontinuous task numbering, maybe it makes sense on the rendered page. Why isn't this TASK 2?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I left this numbering in there so as not to mess with the original tutorials. The ordering makes more sense if you look at the .c, .camkes and .txt files that are generated from the .md file. Should we mention this on the tutorial pages?
The current camkes tutorial overview (https://docs.sel4.systems/Tutorials/#camkes-tutorials) points to a slide presentation, which is no longer available and may have had more detail.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The presentations still seem to be available here: https://github.com/seL4/sel4-tutorials/tree/master/docs. It's in old D61 layout, but the content is still Ok, I think.

/*? macros.simulate_block() ?*/
### Run Hello, World using QEMU

The final image can be run *inside* the container using the command:
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

QEMU is not a container, it is a hardware CPU emulator. The text below already says that it will be run within QEMU simulator, so I'd keep the original text "The final image can be run by:".

Once you have made your change, rerun `ninja` to rebuild the project:
Once you have made your change, use Terminal B to rebuild the project.

*Hint:* Remember to exit the QEMU siumator before rerunning the project with `ctrl-A,x`.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
*Hint:* Remember to exit the QEMU siumator before rerunning the project with `ctrl-A,x`.
*Hint:* Remember to exit the QEMU simulator before rerunning the project with `ctrl-A,x`.


*Hint:* Remember to exit the QEMU siumator before rerunning the project with `ctrl-A,x`.

Then rebuild using ninja and run the simulator again:
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Was this one supposed to replace the next line?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've removed line 208

'mcs-server','mcs-badge','mcs-fault']) ?*/

This tutorial presents the features in the upcoming MCS extensions for seL4, which are currently undergoing
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
This tutorial presents the features in the upcoming MCS extensions for seL4, which are currently undergoing
This tutorial presents the features in the Mixed-Criticality System (MCS) extensions for seL4, which are currently undergoing

@@ -1,7 +1,7 @@
<!--
Copyright 2021 Michael Neises

SPDX-License-Identifier: BSD-2-Clause
SPDX-License-Identifier: CC-BY-SA-4.0
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

CC-BY-SA-4.0 seems to be compatible with BSD-2-Clause, so the above change is probably legal.

Doesn't seem very polite to do though, especially if there are no other changes.


/*- filter ExcludeDocs() -*/
/*? ExternalFile("CMakeLists.txt") ?*/
```
/*-- filter File("main.c") -*/
/*
* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
* Copyright 2024, seL4 Project a Series of LF Projects, LLC.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Legally dubious.

/*-- filter ExcludeDocs() -*/
/*? ExternalFile("CMakeLists.txt") ?*/
```
/*-- filter File("main.c") -*/
/*
* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
* Copyright 2024, seL4 Project a Series of LF Projects, LLC..
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Legally dubious.

@@ -640,9 +697,9 @@ int main(void) {
/*-- endfilter -*/
/*-- filter File("app.c") -*/
/*
* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
* Copyright 2024, seL4 Project a Series of LF Projects, LLC..
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Legally dubious.

@@ -435,9 +485,9 @@ int main(void) {
/*-- endfilter -*/
/*-- filter File("client.c") -*/
/*
* Copyright 2017, Data61, CSIRO (ABN 41 687 119 230).
* Copyright 2024, seL4 Project a Series of LF Projects, LLC..
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Legally dubious.

bbrcknl added 3 commits July 31, 2024 15:59
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
@bbrcknl
Copy link
Author

bbrcknl commented Jul 31, 2024

@Indanz
Minor fixes made to hello-world and mcs as per your suggestions. Original copyright restore for tute files.

Signed-off-by: Birgit Brecknell <b@brck.nl>
@bbrcknl
Copy link
Author

bbrcknl commented Jul 31, 2024

Dynamic libraries filenames need changing. It's on my to-dos for Friday.

template.py Outdated Show resolved Hide resolved
bbrcknl and others added 8 commits August 2, 2024 09:12
Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: bbrcknl <32238793+bbrcknl@users.noreply.github.com>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
bbrcknl and others added 9 commits August 5, 2024 17:15
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Signed-off-by: Birgit Brecknell <b@brck.nl>
Copy link

@Indanz Indanz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for doing this gargantuan job!

I checked the rendered pages and the diff, those look good. I haven't checked whether the commit history makes sense or not. If it's too much of a mess we can always squash it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants