Here are a few key differences between GitHub.dev and Codespaces.
+
Here are a few key differences between GitHub.dev and Codespaces.
-
A GitHub.dev URL looks like github.dev/username/reponame, while a Codespace URL looks like random-word-123randomcharacters789.github.dev.
-
GitHub.dev is quicker to load than a Codespace.
-
GitHub.dev has a much more limited selection of VS Code extensions to use.
-
You can only install applications and execute code on a Codespace.
+
A GitHub.dev URL looks like github.dev/username/reponame, while a Codespace URL looks like random-word-123randomcharacters789.github.dev.
+
+GitHub.dev is quicker to load than a Codespace.
+
+GitHub.dev has a much more limited selection of VS Code extensions to use.
+
You can only install applications and execute code on a Codespace.
-
One similarity between GitHub.dev and Codespaces (besides the obviously similar VS Code user interfaces), is that your work is still private to you and can only be shared with the public (and retained in the long term) by committing and pushing your progress every so often to your GitHub.com repository. The Source Control tool works slightly different in a Codespace, however.
+
One similarity between GitHub.dev and Codespaces (besides the obviously similar VS Code user interfaces), is that your work is still private to you and can only be shared with the public (and retained in the long term) by committing and pushing your progress every so often to your GitHub.com repository. The Source Control tool works slightly different in a Codespace, however.
Note4.1.4.
@@ -253,11 +255,11 @@
Search Results:
In a Codespace, any file with the extension *.ipynb (short for “IPYthon NoteBook”, Jupyter’s original name) will be treated as a Jupyter notebook. When opening this file, you’ll see a notebook interface, and be prompted to “install the recommended ’Python’ extension” if it’s not already enabled - do this.
Then in your notebook file, click the “Select Kernel” button, then “Install/Enable suggested extensions” for Python+Jupyter. You should then have the option to select a “Python environment” such as Python 3.*.*.
If successful, you should be able to enter import sys; print(sys.version) into the displayed text box, and see the result of executing it with Shift+Enter.
There are plenty of existing tutorials on the internet to help you get acquainted with Python and Jupyter now that you have them available to you in your Codespace. But to get you started, I’ve provided one sample notebook 3 that you can upload to your Codespace to break the ice.
Section4.3Previewing GitHub Pages
-
Another useful application of Codespaces is the ability to preview your GitHub Pages site created in Section 3.2. Return to that repository on GitHub.com and create a new Codespace (Note 4.1.2).
+
Another useful application of Codespaces is the ability to preview your GitHub Pages site created in Section 3.2. Return to that repository on GitHub.com and create a new Codespace (Note 4.1.2).
To spin up your live preview, open a terminal by using the Ctrl/Cmd+Shift+` keys. To make sure the necessary software has been installed, type bundle and hit Enter. Then, you can enter jekyll serve to start the preview server.
You’ll see some output, and eventually Server address: http://127.0.0.1:4000. At that time an alert will appear that says “Your application on port 4000 is available”. You can use its “Open in browser” button, or hover over the http://127.0.0.1:4000 link to be given the same option.
This should open a URL such as random-words-123randomletters789-4000.app.github.dev, which will show a live preview of your GitHub Pages site in a new tab. As soon as you make edits in your Codespace tab, you can return to this tab to (within a second or two) see how your edits will update your live site. Note that this URL is private to you, and your public site won’t be updated until you Commit & Sync your changes (Note 4.1.4).
-
Personally, I use GitHub.dev (or even just the GitHub.com edit button) rather than a full Codespace when adding a quick post or making a quick edit on many of my GitHub Pages websites. But the Codespace option is very handy for when bigger changes are necessary, and you want to make sure everything looks just right before pushing it live to the public.
+
Personally, I use GitHub.dev (or even just the GitHub.com edit button) rather than a full Codespace when adding a quick post or making a quick edit on many of my GitHub Pages websites. But the Codespace option is very handy for when bigger changes are necessary, and you want to make sure everything looks just right before pushing it live to the public.
Section4.4Managing Your Codespaces
GitHub users are provided with a limited amount of free Codespace hours and storage each month, with additional resources available to Pro users, including those with the free GitHub Education benefit (Note 2.1.2). If needed, there is the option to pay for additional resources.
@@ -265,7 +267,11 @@
Search Results:
Note4.4.1.
-
To manage your Codespace resources, visit https://github.com/codespaces. You can stop a Codespace temporarily to preserve your hourly quota, and delete a Codespace you don’t plan to use for a while to save on your storage quota. While actively working in a Codespace, you can stop it by pressing Ctrl/Cmd+Shift+P, typing stop current codespace, and confirming.
In any case, a stopped Codespace can be restarted later when you want to resume work, even if you haven’t committed and pushed your changes. (But be warned: a stopped Codespace and its uncommitted changes may be deleted by GitHub after a few days of inactivity, so don’t leave it alone for long.)
A deleted Codespace can always be recreated later based upon your most recent commit.
+
To manage your Codespace resources, visit https://github.com/codespaces. You can stop a Codespace temporarily to preserve your hourly quota, and delete a Codespace you don’t plan to use for a while to save on your storage quota. While actively working in a Codespace, you can stop it by pressing Ctrl/Cmd+Shift+P, typing stop current codespace, and confirming.
In any case, a stopped Codespace can be restarted later when you want to resume work, even if you haven’t committed and pushed your changes. (But be warned: a stopped Codespace and its uncommitted changes may be deleted by GitHub after a few days of inactivity, so don’t leave it alone for long.)
A deleted Codespace can always be recreated later based upon your most recent commit.
Putting it all together, we have seen three ways to access files on your repo. Going from the least easy to edit to the most editable we have: GitHub.com, GitHub.dev, random-codespace-string.github.dev. Here is what these environments look like.
A collaborator for a GitHub repository has the ability to commit and sync changes to the project, as well as adjust certain settings of the repository. GitHub documentation 1 provides some details on the different permissions/abilities that owners have in comparison to collaborators.
Collaborators are added by going to your repository’s Settings tab, using the Collaborators link in the sidebar. Each collaborator will need their own GitHub account, and must accept the invitation to collaborate before gaining access.
-
Once they have access, a collaborator can either use GitHub.dev (Note 2.4.2) or create their own Codespace (Definition 4.1.1).
+
Once they have access, a collaborator can either use GitHub.dev (Note 2.4.2) or create their own Codespace (Definition 4.1.1).
Warning5.2.2.
If two collaborators on the same repository make commits on the same branch, they will desynchronize your project’s history: person A’s history will think that commit X is followed by Y on branch main, but person B’s history will think that commit X is followed by Z on branch main.
As seen in Figure 1.1.1, Git is meant to support non-linear history. However, to support this, contributors must name their distinct branches.
Note5.2.3.
-
One workflow to support multiple collaborators on the same repository is to never directly commit to the main branch, even if you’re the owner.
To commit to an alternative branch in GitHub.dev or Codespaces, select main in the bottom toolbar, then type the name of your new branch, and select “Create new branch”. The name of this branch could be topical, e.g. add-derivative-chapter, but it’s also fine to pick some other unique identifier, e.g. lastname-YYYY-MM-DD.
Once a collaborator is working on a branch, they are free to edit as they wish, and can (and should) commit and push/sync with GitHub to persist their contributions to the team’s repository.
+
One workflow to support multiple collaborators on the same repository is to never directly commit to the main branch, even if you’re the owner.
To commit to an alternative branch in GitHub.dev or Codespaces, select main in the bottom toolbar, then type the name of your new branch, and select “Create new branch”. The name of this branch could be topical, e.g. add-derivative-chapter, but it’s also fine to pick some other unique identifier, e.g. lastname-YYYY-MM-DD.
Once a collaborator is working on a branch, they are free to edit as they wish, and can (and should) commit and push/sync with GitHub to persist their contributions to the team’s repository.
To facilitate communication among collaborators working on different branches, it’s good practice to open a draft pull request once a new branch is created.
Definition5.2.4.
@@ -236,7 +236,7 @@
Search Results:
A pull request (or PR for short) is a discussion thread for a branch that proposes changes to a different (often, the main) branch. When the branch’s changes are ready to be merged, this can be accomplished by pressing a button on the pull request webpage.
A PR can be marked as a draft or ready to review.
Note5.2.5.
-
Depending on whether the collaborator is using GitHub.dev or Codespaces, they may be prompted to create a pull request when first pushing/syncing changes. If not, a pull request can be created by navigating to the repository page on GitHub.com.
Recent pushes to a branch will reveal a prompt to create the pull request immediately. Otherwise, the PR can be created by using the Pull Requests tab of the page.
Unless the PR is for a single commit that’s immediately “ready for review”, a new PR should be created as a draft.
With a draft pull request created, the contributor can continue to commit and push/sync to the branch until it is ready for review. The discussion features of GitHub can allow contributors to discuss the proposed changes, whether they are in draft or review-ready status.
+
Depending on whether the collaborator is using GitHub.dev or Codespaces, they may be prompted to create a pull request when first pushing/syncing changes. If not, a pull request can be created by navigating to the repository page on GitHub.com.
Recent pushes to a branch will reveal a prompt to create the pull request immediately. Otherwise, the PR can be created by using the Pull Requests tab of the page.
Unless the PR is for a single commit that’s immediately “ready for review”, a new PR should be created as a draft.
With a draft pull request created, the contributor can continue to commit and push/sync to the branch until it is ready for review. The discussion features of GitHub can allow contributors to discuss the proposed changes, whether they are in draft or review-ready status.
Note5.2.6.
@@ -274,7 +274,7 @@
Search Results:
Note5.3.2.
-
To create a fork of a public repository, press the “Fork” button on its GitHub.com homepage. You can name this fork whatever you like, it will be tracke don GitHub as a fork of the original project, with the ability to make “upstream” contributions by way of pull requests.
Those of us who work in open source typically love getting pull requests from random collaborators. For example, if you find a typo in this book, you can fxi it by creating a fork at https://github.com/StevenClontz/github-for-mathematicians/fork, editing the appropriate source/*.ptx file to fix the word, and open a pull request.
+
To create a fork of a public repository, press the “Fork” button on its GitHub.com homepage. You can name this fork whatever you like, it will be tracke don GitHub as a fork of the original project, with the ability to make “upstream” contributions by way of pull requests.
Those of us who work in open source typically love getting pull requests from random collaborators. For example, if you find a typo in this book, you can fxi it by creating a fork at https://github.com/StevenClontz/github-for-mathematicians/fork, editing the appropriate source/*.ptx file to fix the word, and open a pull request.
The last option we’ll make sure to select is to “Initialize this repository with: Add a README file”. Then click “Create repository”.
Section2.3Editing README.md
-
While logged into GitHub.com, you have the ability to edit individual files on your repositories. (If your repository is public, others can see those files, but cannot edit them unless you make them a collaborator, see Chapter 5.)
+
While logged into GitHub.com, you have the ability to edit individual files on your repositories. (If your repository is public, others can see those files, but cannot edit them unless you make them a collaborator, see Chapter 5.)
An easy way to edit an individual file is just to click the pencil icon such as the one that appears on your README. This file is written in Markdown, a markup language that takes plain text like *this* and renders it “like this”.
Try to edit your file to say something like “I’m learning how to use GitHub!”, perhaps adding a link back to this document using [this markup](https://g4m.clontz.org). You can click the Preview tab to see what your README will look like, and visit sites like https://www.MarkdownTutorial.com or https://www.MarkdownGuide.org to learn more. GitHub also provides a panel of several formatting options you can click on.
-
When you’re happy with your updated README, click the “Commit changes” button. This will create a new commit, representing a new moment in your project’s history. You should write a useful commit message summarizing the work you’ve done since your last commit (or perhaps keep the default “Update README.md”) Doing this will update the README visible on your repository homepage on GitHub.com.
+
When you’re happy with your updated README, click the “Commit changes” button. This will create a new commit, representing a new moment in your project’s history. You should write a useful commit message summarizing the work you’ve done since your last commit (or perhaps keep the default “Update README.md”) Doing this will update the README visible on your repository homepage on GitHub.com.
Finally, you might be interested in visiting the “Insights” tab for your repository, and specifically the “Network” page. It should reveal a graphic similar to Figure 1.1.1 visualizing the history of you project across all GitHub collaborators. Right now you don’t have any collaborators and just a couple commits, but keeping in mind this model for your project history will be useful as we juggle various commits and pushes and syncs and so on down the line.
Section2.4Using GitHub.dev
-
Using the GitHub.com interface to author or edit just one file can be useful (I do this all the time to make quick typo fixes on my blog), but you will likely be using GitHub to manage projects that involve editing mulitple files at the same time, and likely you will have non-text files (such as images) that you need to include in your work as well.
+
Using the GitHub.com interface to author or edit just one file can be useful (I do this all the time to make quick typo fixes on my blog), but you will likely be using GitHub to manage projects that involve editing mulitple files at the same time, and likely you will have non-text files (such as images) that you need to include in your work as well.
One way to quickly be able to manage several files at once is to use the GitHub.dev 1 service offered by GitHub. Try clicking that link - you should have a fully-functional VS Code text editor right inside your web browser.
Note2.4.1.
-
It’s best to use an updated version of Chrome, Edge, or Firefox when using GitHub. In particular, Safari tends to show off its rough edges when using advanced web applications like GitHub.dev, so it’s best to choose an alternative.
You can create files, edit them, upload images, and do whatever you like at GitHub.dev. But this isn’t your repository - it’s just an example. So, we’ll need a way to tell GitHub.dev we want to work on the repository we just made instead.
+
It’s best to use an updated version of Chrome, Edge, or Firefox when using GitHub. In particular, Safari tends to show off its rough edges when using advanced web applications like GitHub.dev, so it’s best to choose an alternative.
You can create files, edit them, upload images, and do whatever you like at GitHub.dev. But this isn’t your repository - it’s just an example. So, we’ll need a way to tell GitHub.dev we want to work on the repository we just made instead.
Note2.4.2.
-
There are two very easy ways to access the GitHub.dev service. The first is to just change the address of your repository from github.com to github.dev in your browser. For example, if your repository lives at https://github.com/YourUserName/YourGreatRepo, you should visit https://github.dev/YourUserName/YourGreatRepo.
The other trick is even fancier. When you are visiting https://github.com/YourUserName/YourGreatRepo in your web browser and not writing in a text box, press the period (.) key.
Either way, you should now have a GitHub.dev window where you can manage all the files of your project. Using the Explorer sidebar (Figure 2.4.3), you can create new files, rename files, move files, upload files, and more. Selecting a file opens it, and lets you edit it as needed. Your changes are saved automatically in GitHub.dev, but they won’t show up at GitHub.com just yet.
-
Section2.5Commiting Your Work
After you’re tried creating/editing/uploading a few files, now it’s time to commit those changes to your repository. The easiest way to do this is to use the Source Control sidebar. You may have noticed that a numerical badge appeared by the Source Control icon as you created, edited, or deleted files. This number represents the number of files that have been changed in some way since the previous commit. By opening the Source Control panel, you’ll see a list of these files.
Clicking these file names not only lets you open the file and edit it further, but you are shown a diff - a summary of the lines that have been altered since the previous commit. (This is a good reason to not write in a long continuous line, but to break lines every 80ish characters or so. That way you can easily see where exactly a change is made between each commit.)
-
The idea is this: edit as you see fit, knowing that your files are being saved at GitHub.dev and won’t be lost if you accidentally refresh your web browser. However, you’ll need to eventually commit those changes to the repository in order to share your work with anyone else, and to ensure that the work is preserved in the long term. The Source Control panel provides a place to write a commit message, a short phrase or sentence that summarizes the work you’ve done. (Writer’s block? For now just type “learning GitHub.dev”.) Then once you click the “Commit and Push” button, your work will be logged as a permanent commit to the repository.
-
This is a good point to review your commit history again. You probably have three commits: the initial commit made when you created the repository, the README.md update you made using GitHub.com’s editing interface, and this more elaborate GitHub.dev commit involving possibly several files. To visualize this history, you can go to the Insights/Network page described earlier, or click on the “3 commits” link from your GitHub.com repository homepage to see a linearization of this history. From there you can click on each commit to see exactly what has changed from the previous commit across all files.
+
The idea is this: edit as you see fit, knowing that your files are being saved at GitHub.dev and won’t be lost if you accidentally refresh your web browser. However, you’ll need to eventually commit those changes to the repository in order to share your work with anyone else, and to ensure that the work is preserved in the long term. The Source Control panel provides a place to write a commit message, a short phrase or sentence that summarizes the work you’ve done. (Writer’s block? For now just type “learning GitHub.dev”.) Then once you click the “Commit and Push” button, your work will be logged as a permanent commit to the repository.
+
This is a good point to review your commit history again. You probably have three commits: the initial commit made when you created the repository, the README.md update you made using GitHub.com’s editing interface, and this more elaborate GitHub.dev commit involving possibly several files. To visualize this history, you can go to the Insights/Network page described earlier, or click on the “3 commits” link from your GitHub.com repository homepage to see a linearization of this history. From there you can click on each commit to see exactly what has changed from the previous commit across all files.
Importantly, GitHub is not itself open-source software, but is a service owned and operated by Microsoft. However, Microsoft makes GitHub available for use at no cost to the public, with additional “pro” features available for free to instructors and researchers.
We’ll use GitHub not only as a host for our repositories, but also to take advantage of all the tools it provides to author content using only a web browser. If you’ve looked into using Git in the past, you may have hesitated due to the apparent need for software developer experience to get started. However, using GitHub’s web applications, there will be no need for complicated installations or memorizing command line incantations like git commit -m "foobar" to type into a terminal. (Of course, you still can choose to use such tools to get as much control over your Git project as you want, should the need ever arise: see Appendix B)
Another reason to use GitHub: community! GitHub is often marketed as a “social coding platform”, because it not only provides tools to create and deliver digital content, but it also provides social features such as Following users, Starring repositories, participation in Discussions and Issues, and more. Particular in open-source, we like to work together and support each other, and GitHub provides much of the social cyberinfrastructure necessary to do so efficiently.
-Section1.3G4M on GitHub.com
+Section1.3G4M on GitHub.com
An example of a project using Git and GitHub is the document you’re reading right now! This book is open-sourced and shared at https://github.com/StevenClontz/github-for-mathematicians, and was authored completely in a web browser using only the GitHub features we will explore together in this handbook.
I recommend you add a link to your GitHub.io website from your GitHub.com repository page.
-Note3.1.3.
+Note3.1.4.
On your repository page, you can edit the “About” sidebar to add useful information about your project. In particular, there’s a checkbox to automatically display your GitHub.io link to make it easy for others (and yourself!) to find your GitHub Pages site.
Section3.2Using a Template
@@ -265,18 +267,20 @@
Search Results:
Definition3.2.1.
A template repository on GitHub provides other GitHub users the ability to easily obtain a shallow copy of the latest commit to the template, created as a new repository they control.
This is meant for situations like a GitHub Pages website, where you probably don’t care about every single change that was made to create the template you’re using, and you don’t plan on contributing any of your changes back to the original repository. Instead, you just want the latest working files so you can insert your own content and get it online.
-
Visit this page 1 and click “Use this template”, and “Create a new repository”. This creates a new repository you own on GitHub.com, and you can follow the instructions in Note 3.1.1 to enable GitHub Pages. Once that’s done, visit your new GitHub.io website to see the placeholder content of your new website (don’t forget to add a link to your “About” sidebar, see Note 3.1.3).
+
Visit this page 1 and click “Use this template”, and “Create a new repository”. This creates a new repository you own on GitHub.com, and you can follow the instructions in Note 3.1.1 to enable GitHub Pages.
+Figure3.2.2.Use this template button. Once that’s done, visit your new GitHub.io website to see the placeholder content of your new website (don’t forget to add a link to your “About” sidebar, see Note 3.1.4).
-Note3.2.2.
+Note3.2.3.
-
Deploying to GitHub Pages can take some time, so visiting the “Actions” tab on your repository page will let you see how this process is progressing. You can also see the status of this process by looking for the following icon next to your commit message: an orange dot (in progress), a green checkmark (deployed), or a red X (failure).
+
Deploying to GitHub Pages can take some time, so visiting the “Actions” tab on your repository page will let you see how this process is progressing. You can also see the status of this process by looking for the following icon next to your commit message: an orange dot (in progress), a green checkmark (deployed), or a red X (failure).
+Figure3.2.4.Actions tab on Github.com.
Section3.3Customizing Your Site
Now that you have the template website hosted by GitHub Pages, you of course will want to customize it to yourself. For this book, I’ll get you started by handling a few of the obvious first steps, assuming you’re using the GitHub.dev service (Note 2.4.2).
Subsection3.3.1Configuration
First things first, let’s configure some basic elements of your site. These settings are found in /_config.yml. There are several pieces of this file you likely aren’t interested in editing (nor do you need to know at this point what they do), but you should at least find the title: and description: lines and edit them with your own information. The same goes for the author: name: and author: bio: entries as well.
-
To see that this worked, use Source Control to Commit and Push your edits. After a while (Note 3.2.2) you should be able to refresh your website and see your updated title, name, etc. (In Section 4.3, we will learn how to preview our edits more quickly, and without needing to push them to a live website, but at the expense of a more complicated editing environment.) You can repeat this process after each of the edits described below to see your results reflected on the live website.
+
To see that this worked, use Source Control to Commit and Push your edits. After a while (Note 3.2.3) you should be able to refresh your website and see your updated title, name, etc. (In Section 4.3, we will learn how to preview our edits more quickly, and without needing to push them to a live website, but at the expense of a more complicated editing environment.) You can repeat this process after each of the edits described below to see your results reflected on the live website.
Subsection3.3.2Photo
Next, let’s add your photo. A placeholder is available at /assets/images/bio-photo.jpg. You can drag your own JPG-format photo onto it in the File Explorer. Then you can delete the placeholder bio-photo.jpg and rename your photo to bio-photo.jpg.
@@ -290,11 +294,14 @@
Search Results:
---
Listing3.3.1.About page metadata
Below the metadata is Markdown source that can be edited to include whatever content you’d like to appear within the page.
-
To create additional pages, copy-paste about.md to create new files in the /_pages/ directory, making sure to assign each page its own permalink. If you want these pages to appear in the navigation bar on top of your site, edit the /_data/navigation.yml configuration file to point to each permalink.
+
To create additional pages, copy-paste about.md to create new files in the /_pages/ directory, making sure to assign each page its own permalink. If you want these pages to appear in the navigation bar on top of your site, edit the /_data/navigation.yml configuration file to point to each permalink.
+
You can preview a compiled version of your markdown files (.md ) on the web, without having to run any commands. It is enough to open a markdown file and split the screen.
+
+Figure3.3.2.Split screen to preview markdown file.
Subsection3.3.4Posts
Posts are similar to pages, and live in the /_posts/ directory. To create a new post, copy-paste any of the existing post files and rename it into the form YYYY-MM-DD-my-new-post.md (where YYYY-MM-DD is the date you want associated with the post).
-
The content of your post is just Markdown, as with pages. However, you have slightly different metadata to edit (Listing 3.3.2). In the date you can set the specific time of day you want your post to be associated with. You can also choose to assign each post categories and tags, which allow your posts to be sorted into appropriate category and tag pages, which are generated automatically for you.
+
The content of your post is just Markdown, as with pages. However, you have slightly different metadata to edit (Listing 3.3.3). In the date you can set the specific time of day you want your post to be associated with. You can also choose to assign each post categories and tags, which allow your posts to be sorted into appropriate category and tag pages, which are generated automatically for you.