ATMxsp01

1
from dataclasses import dataclass
2
from typing import Iterable
3

4
import torch
5

6

7
@dataclass(frozen=True)
8
class Sample:
9
    """一条训练样本。"""
10
    text: str
11
    label: int
12

13

14
def batchify(samples: Iterable[Sample], size: int = 32) -> list[list[Sample]]:
15
    batch: list[Sample] = []
16
    for item in samples:
17
        batch.append(item)
18
        if len(batch) == size:      # 满一批就吐出
19
            yield batch
20
            batch = []
21
    if batch:
22
        yield batch
23

24

25
if __name__ == "__main__":
26
    total = sum(1 for _ in batchify([Sample(f"x{i}", i % 2) for i in range(100)]))
27
    print(f"batches = {total}, cuda = {torch.cuda.is_available()}")

1
#include <algorithm>
2
#include <iostream>
3
#include <queue>
4
#include <vector>
5

6
namespace graph {
7

8
template <typename T>
9
class BFS {
10
public:
11
    explicit BFS(const std::vector<std::vector<int>>& adj) : adj_(adj) {}
12

13
    std::vector<int> run(int src) const {
14
        std::vector<int> dist(adj_.size(), -1);
15
        std::queue<int> q;
16
        dist[src] = 0;
17
        q.push(src);
18
        while (!q.empty()) {
19
            const int u = q.front();
20
            q.pop();
21
            for (const int v : adj_[u]) {
22
                if (dist[v] == -1) {          // 未访问
23
                    dist[v] = dist[u] + 1;
24
                    q.push(v);
25
                }
26
            }
27
        }
28
        return dist;
29
    }
30

31
private:
32
    const std::vector<std::vector<int>>& adj_;
33
};
34

35
}  // namespace graph
36

37
int main() {
38
    const std::vector<std::vector<int>> adj{{1, 2}, {3}, {3}, {}};
39
    const auto dist = graph::BFS<int>(adj).run(0);
40
    for (std::size_t i = 0; i < dist.size(); ++i)
41
        std::cout << "dist[" << i << "] = " << dist[i] << '\n';
42
    return 0;
43
}

1
use std::collections::HashMap;
2
use std::hash::Hash;
3

4
#[derive(Debug, Default)]
5
pub struct LruCache<K, V> {
6
    map: HashMap<K, V>,
7
    capacity: usize,
8
    hits: u64,
9
}
10

11
impl<K: Eq + Hash + Clone, V: Clone> LruCache<K, V> {
12
    pub fn new(capacity: usize) -> Self {
13
        assert!(capacity > 0, "capacity must be positive");
14
        Self { map: HashMap::new(), capacity, hits: 0 }
15
    }
16

17
    pub fn get(&mut self, key: &K) -> Option<&V> {
18
        match self.map.get(key) {
19
            Some(value) => {
20
                self.hits += 1;
21
                Some(value)
22
            }
23
            None => None,
24
        }
25
    }
26

27
    pub fn insert(&mut self, key: K, value: V) -> Result<(), String> {
28
        if self.map.len() >= self.capacity && !self.map.contains_key(&key) {
29
            return Err(format!("cache full: {} entries", self.capacity));
30
        }
31
        self.map.insert(key, value);
32
        Ok(())
33
    }
34

35
    pub fn hit_rate(&self) -> f64 {
36
        if self.map.is_empty() { 0.0 } else { self.hits as f64 / self.map.len() as f64 }
37
    }
38
}

1
#!/usr/bin/env bash
2
set -euo pipefail
3

4
REPO="${1:-ATMxsp01/blog-content}"
5
BRANCH="${BRANCH:-main}"
6

7
echo "==> 同步 $REPO ($BRANCH)"
8
if ! git -C "$REPO" diff --quiet; then
9
    echo "工作树不干净，先提交" >&2
10
    exit 1
11
fi
12

13
for step in sync validate build; do
14
    printf '  -> %s ... ' "$step"
15
    pnpm "content:$step" >/dev/null 2>&1 && echo "ok" || { echo "failed"; exit 1; }
16
done
17

18
# 统计产物
19
find dist -name '*.html' | wc -l | xargs printf 'pages: %s\n'
20
echo "done in ${SECONDS}s"

1
import Mathlib.Data.Nat.Basic
2

3
namespace Demo
4

5
/-- 归纳定义的偶数谓词。 -/
6
inductive Even : Nat → Prop
7
  | zero : Even 0
8
  | add_two {n : Nat} : Even n → Even (n + 2)
9

10
theorem even_add (m n : Nat) (hm : Even m) (hn : Even n) : Even (m + n) := by
11
  induction hm with
12
  | zero => simpa using hn
13
  | add_two _ ih => simpa [Nat.add_assoc] using Even.add_two ih
14

15
def double (n : Nat) : Nat := n * 2
16

17
example (n : Nat) : double n = n + n := by
18
  simp [double, Nat.mul_two]   -- 一条 tactic 搞定
19

20
end Demo