erikmd

# This file was generated from `meta.yml`, please do not edit manually.
# Follow the instructions on https://github.com/coq-community/templates to regenerate.
name: Docker CI

on:
  push:
    branches:
      - main
      - ITP2023
  pull_request:

erikmd

Magit/Forge and GitHub

Magit

erikmd

#!/bin/bash

usage="
Usage:
 wall [options] [message]

Write a message to all users.

Options:
 -n, --nobanner          do not print banner

erikmd

Running with gitlab-runner 15.6.0~beta.186.ga889181a (a889181a)
  on blue-2.shared.runners-manager.gitlab.com/default XxUrkriX
section_start:1668295707:prepare_executor
Preparing the "docker+machine" executor
Using Docker executor with image docker:latest ...
Starting service docker:dind ...
Pulling docker image docker:dind ...
Using docker image sha256:5daac9489dc300a47bcb0ea96855ff17e5353aaab9065dbe19b890f480626683 for docker:dind with digest docker@sha256:659bd125658c3f2a28d1a51418853cf85c439df863e3eff0dcc3a0c30feadbb6 ...
Waiting for services to be up and running (timeout 30 seconds)...
Pulling docker image docker:latest ...

erikmd

Running with gitlab-runner 15.6.0~beta.186.ga889181a (a889181a)
  on blue-3.shared.runners-manager.gitlab.com/default zxwgkjAP
section_start:1668296743:prepare_executor
Preparing the "docker+machine" executor
Using Docker executor with image docker:latest ...
Starting service docker:dind ...
Pulling docker image docker:dind ...
Using docker image sha256:5daac9489dc300a47bcb0ea96855ff17e5353aaab9065dbe19b890f480626683 for docker:dind with digest docker@sha256:659bd125658c3f2a28d1a51418853cf85c439df863e3eff0dcc3a0c30feadbb6 ...
Waiting for services to be up and running (timeout 30 seconds)...
Pulling docker image docker:latest ...

erikmd

C99 List of Undefined Behavior

From N1256: (See http://port70.net/~nsz/c/c99/n1256.html#J.2)

• A "shall" or "shall not" requirement that appears outside of a constraint is violated (clause 4).
• A nonempty source file does not end in a new-line character which is not immediately preceded by a backslash character or ends in a partial preprocessing token or comment (5.1.1.2).
• Token concatenation produces a character sequence matching the syntax of a universal character name (5.1.1.2).
• A program in a hosted environment does not define a function named main using one of the specified forms (5.1.2.2.1).
• A character not in the basic source character set is encountered in a source file, except in an identifier, a character constant, a string literal, a header name, a comment, or a preprocessing token that is never converted to a token (5.2.1).
• An identifier, comment, string literal, character constant, or header name contains an invalid multibyte character or does not

erikmd

#!/usr/bin/env python3
"""
License: MIT License
Copyright (c) 2023 Miel Donkers

Very simple HTTP server in python for logging requests
Usage::
    ./server.py [<port>]
"""
from http.server import BaseHTTPRequestHandler, HTTPServer

erikmd

(* Rappel syntaxe Coq : les commentaires s'écrivent entre (* et *). *)

(******************************)
(* Tutoriel (Cours/TP) de Coq *)
(******************************)

(* Voir aussi ces supports de Cours (UE ILU3, L3 Info, UPS) :

   https://pfitaxel.github.io/ilu3-coq-alectryon/

erikmd

1. Create SSH keypair

In order to deploy using SSH, we need a SSH keypair. Please use an algorithm strong enough and also supported by GHA and your remote host.

You can use the command below to generate a keypair:

ssh-keygen -t ed25519 -C gha@vm-YourLogin -f ~/.ssh/id_gha

For this use case, don't use a passphrase (just type Return to select an empty passphrase).

erikmd

Recommended Git configuration

Run these standard commands anytime you setup git on a new workstation.

Mandatory

git config --global user.name "Prénom Nom"
git config --global user.email "prenom.nom@example.com"