Skip to content

How to submit homework

You will submit homework on faculty GitLab. New to GitLab? Start with the extra instructions below.

If you have used GitLab before

  1. Sign in to faculty GitLab and go to this page. You should see there your version of the class repo (your private fork). If you don't, see extra instructions below.

  2. An ugly shortcut is to submit the homework (file hw1.lean for the first one) via web interface, navigate in your repository to LeanComputerAssistedProofs2026/Submissions. Press the "+" sign, "Upload file", "Commit changes". In principle, you can use this method & the live-lean server if you don't have a computer with Lean available right now. (Not advisable long term!)

  3. The proper way (in the long term anyway) is to change origin in your local course repository. (You may clone the gitlab project and start fresh, but that will repeat the download/compile of all the mathlib files, you don't want that.) In your project's Code you find your "clone URL". Use SSH if you already have an SSH key registered on this server; otherwise use HTTPS and follow the authentication instructions. Run this in a terminal (you may open it inside VS Code). YOUR_PRIVATE_PROJECT_CLONE_URL should be replaced by your own. 

    git remote set-url origin YOUR_PRIVATE_PROJECT_CLONE_URL
git config pull.rebase false

  4. Work on branch main. Homework problems will be in folder LeanComputerAssistedProofs2026/Homeworks/, you submit the edited version in LeanComputerAssistedProofs2026/Submissions/.

  5. Save, commit, pull, and push. You most likely know how to do this (inside VS Code or other tools you are using). If you are new to this: For homework 1, assuming you didn't do any changes to the files from lectures. 

    git add LeanComputerAssistedProofs2026/Submissions/hw1.lean
git commit -m "Submit homework 1"
git pull --no-rebase --ff origin main
git push -u origin main
    If you changed files in the LectureXX folder, you may commit your changes or rename them, so that you get both your and my version. Do this before pulling. If you are unsure how to resolve git conflicts, ask for help. (AI chatbots are very good at this.)

  6. For the first homework, just to be sure, check in browser the contents of the submitted file via web interface, navigate in your repository to LeanComputerAssistedProofs2026/Submissions.

Extra instructions for first-time users

1. Activate your account

  • Sign in at gitlab.mff.cuni.cz using your CAS credentials, as for SIS. Use your name-based username, not your numerical student ID.
  • Then send me an email, I will need to add your new account to your project. (See the faculty login instructions if you have trouble signing in.)
  • Once you are added, proceed as in the description above.
  • There is one extra step needed: tell your VS Code that you are you:

2. Authenticate from VS Code

Signing in to GitLab in your browser does not sign Git in. For this, create a personal access token: a GitLab-generated password for Git.

  1. Open Personal access tokens in GitLab. Choose Generate token → Legacy token.
  2. Give it a name such as Lean course, choose an expiration date after the course ends, and select the write_repository scope. This permits both pulling and pushing; api is not needed.
  3. Generate the token and save it securely (treat it as a password). You will only see it once from GitLab (you can generate a new one if needed).
  4. Back in VS Code, open the Command Palette with F1 and run Git: Fetch. Fetch checks the connection without changing your working files.
  5. When asked for credentials, enter your GitLab username and paste the token into the password field. Depending on your system, this prompt may appear in VS Code or in a separate credential-manager window. Your credential manager may save it for later use.

VS Code's built-in Git support is enough, no extension is needed.

If something goes wrong

  • Cannot open your private project in the browser: let me know your GitLab username. You may still need to be added to the project.
  • Authentication failed: check that you used the token as the HTTPS password, that it has not expired, and that it has write_repository permission. An SSH URL (git@…) uses SSH keys instead of a token.
  • Pull reports conflicts, or Push is rejected: you have different version of files in your local folder than in the repo. As a temporary workaround, you may submit using gitlab web interface as described above. The proper solution is to synchronize your files with the repository. Or other situations, ask for help with the exact error message. (Me or your favorite AI.) You can temporarily submit through the web interface.
  • VS Code offers “Publish to GitHub”: check that you opened the existing course folder and changed its origin to your private GitLab project. Your submission project already exists.
  • If Git asks you to configure your name and email (you haven't used git before, for instance): Run these once in the course folder, using your own details: 
    git config user.name "Your Full Name"
git config user.email "your.email@example.org"